diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index 48bed0da19..cf4142b6ca 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -241,6 +241,8 @@ def mkFreshExprMVar (ref : Syntax) (type? : Option Expr := none) (kind : Metavar
 match type? with
 | some type => liftMetaM ref $ Meta.mkFreshExprMVar type userName? kind
 | none      => liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; type ← Meta.mkFreshExprMVar (mkSort u); Meta.mkFreshExprMVar type userName? kind
+def mkFreshTypeMVar (ref : Syntax) (kind : MetavarKind := MetavarKind.natural) (userName? : Name := Name.anonymous) : TermElabM Expr :=
+liftMetaM ref $ do u ← Meta.mkFreshLevelMVar; Meta.mkFreshExprMVar (mkSort u) userName? kind
 def getLevel (ref : Syntax) (type : Expr) : TermElabM Level := liftMetaM ref $ Meta.getLevel type
 def mkForall (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkForall xs e
 def mkLambda (ref : Syntax) (xs : Array Expr) (e : Expr) : TermElabM Expr := liftMetaM ref $ Meta.mkLambda xs e
@@ -392,7 +394,7 @@ def expandCDot? : Syntax → TermElabM (Option Syntax)
 
 private def exceptionToSorry (ref : Syntax) (ex : Elab.Exception) (expectedType? : Option Expr) : TermElabM Expr := do
 expectedType : Expr ← match expectedType? with
-  | none              => mkFreshExprMVar ref
+  | none              => mkFreshTypeMVar ref
   | some expectedType => pure expectedType;
 u ← getLevel ref expectedType;
 let syntheticSorry := mkApp2 (mkConst `sorryAx [u]) expectedType (mkConst `Bool.true);
@@ -814,7 +816,7 @@ fun stx expectedType? => do
   val ← match (stx.getArg 0).isNatLit? with
     | some val => pure (mkNatLit val)
     | none     => throwError stx.val "ill-formed syntax";
-  typeMVar ← mkFreshExprMVar ref none MetavarKind.synthetic;
+  typeMVar ← mkFreshTypeMVar ref MetavarKind.synthetic;
   registerSyntheticMVar ref typeMVar.mvarId! (SyntheticMVarKind.withDefault (Lean.mkConst `Nat));
   match expectedType? with
   | some expectedType => do isDefEq ref expectedType typeMVar; pure ()