From bdc9ea6fc6f6987f540fefd54bc8d1b0a1527910 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 19 Dec 2019 09:58:05 -0800
Subject: [PATCH] fix: unregistered level metavariable

---
 src/Init/Lean/Meta/InferType.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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