diff --git a/src/Init/Lean/Util/Message.lean b/src/Init/Lean/Util/Message.lean
index 4e40aad34f..379eab12b0 100644
--- a/src/Init/Lean/Util/Message.lean
+++ b/src/Init/Lean/Util/Message.lean
@@ -63,7 +63,7 @@ partial def formatAux : Option MessageDataContext → MessageData → Format
 | some ctx,  ofSyntax s        => s.formatStx (getSyntaxMaxDepth ctx.opts)
 | none,      ofSyntax s        => s.formatStx
 | none,      ofExpr e          => format (toString e)
-| some ctx,  ofExpr e          => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts e -- TODO: replace with new pretty printer
+| some ctx,  ofExpr e          => ppOld ctx.env ctx.mctx ctx.lctx ctx.opts (ctx.mctx.instantiateMVars e).1 -- TODO: replace with new pretty printer
 | _,         withContext ctx d => formatAux (some ctx) d
 | ctx,       tagged cls d      => Format.sbracket (format cls) ++ " " ++ formatAux ctx d
 | ctx,       nest n d          => Format.nest n (formatAux ctx d)