diff --git a/src/Init/Lean/Meta/InferType.lean b/src/Init/Lean/Meta/InferType.lean
index 30e5e5574d..a52932ec4d 100644
--- a/src/Init/Lean/Meta/InferType.lean
+++ b/src/Init/Lean/Meta/InferType.lean
@@ -75,8 +75,7 @@ match typeType with
 | Expr.mvar mvarId _ =>
   condM (isReadOnlyOrSyntheticOpaqueExprMVar mvarId)
     (throwEx $ Exception.typeExpected type)
-    (do levelMVarId ← mkFreshId;
-        let lvl := mkLevelMVar levelMVarId;
+    (do lvl ← mkFreshLevelMVar;
         assignExprMVar mvarId (mkSort lvl);
         pure lvl)
 | _ => throwEx $ Exception.typeExpected type