diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index d7a0d6112c..86968ee1d3 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -494,8 +494,6 @@ fun stx => do
     e    ← Term.elabTerm term none;
     Term.synthesizeSyntheticMVars false;
     type ← Term.inferType stx.val e;
-    e    ← Term.instantiateMVars stx.val e;
-    type ← Term.instantiateMVars stx.val type;
     logInfo stx.val (e ++ " : " ++ type);
     pure ()