diff --git a/src/Lean/Delaborator.lean b/src/Lean/Delaborator.lean
index 3b6e05ee6b..35998eb386 100644
--- a/src/Lean/Delaborator.lean
+++ b/src/Lean/Delaborator.lean
@@ -247,6 +247,7 @@ pure $ mkIdent l.userName
 @[builtinDelab mvar]
 def delabMVar : Delab := do
 Expr.mvar n _ ← getExpr | unreachable!;
+let n := n.replacePrefix `_uniq `m;
 `(?$(mkIdent n))
 
 @[builtinDelab sort]