diff --git a/src/Lean/Elab/Inductive.lean b/src/Lean/Elab/Inductive.lean
index 5bbbf32707..42a1fba10e 100644
--- a/src/Lean/Elab/Inductive.lean
+++ b/src/Lean/Elab/Inductive.lean
@@ -250,11 +250,9 @@ r.view.ctors.toList.mapM fun ctorView => Term.elabBinders ctorView.binders.getAr
    `inferResultingUniverse`. -/
 private def levelMVarToParamAux (ref : Syntax) (indTypes : List InductiveType) : StateT Nat TermElabM (List InductiveType) :=
 indTypes.mapM fun indType => do
-  type  ← liftM $ Term.instantiateMVars ref indType.type;
-  type  ← Term.levelMVarToParam' type;
+  type  ← Term.levelMVarToParam' indType.type;
   ctors ← indType.ctors.mapM fun ctor => do {
-    ctorType ← liftM $ Term.instantiateMVars ref ctor.type;
-    ctorType ← Term.levelMVarToParam' ctorType;
+    ctorType ← Term.levelMVarToParam' ctor.type;
     pure { ctor with type := ctorType }
   };
   pure { indType with ctors := ctors, type := type }
diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 6a83da7f5b..7baa97fdb2 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -1011,7 +1011,7 @@ partial def visitLevel : Level → M Level
     pure p
 
 @[inline] private def visit (f : Expr → M Expr) (e : Expr) : M Expr :=
-if e.hasLevelMVar then f e else pure e
+if e.hasMVar then f e else pure e
 
 partial def main : Expr → M Expr
 | e@(Expr.proj _ _ s _)    => do s ← visit main s; pure (e.updateProj! s)
@@ -1022,6 +1022,11 @@ partial def main : Expr → M Expr
 | e@(Expr.mdata _ b _)     => do b ← visit main b; pure (e.updateMData! b)
 | e@(Expr.const _ us _)    => do us ← us.mapM visitLevel; pure (e.updateConst! us)
 | e@(Expr.sort u _)        => do u ← visitLevel u; pure (e.updateSort! u)
+| e@(Expr.mvar mvarId _)   => do
+  s ← get;
+  match s.mctx.getExprAssignment? mvarId with
+  | some v => visit main v
+  | none   => pure e
 | e                        => pure e
 
 end LevelMVarToParam