diff --git a/src/Lean/MetavarContext.lean b/src/Lean/MetavarContext.lean
index 8bd8f9ab98..775dc666b5 100644
--- a/src/Lean/MetavarContext.lean
+++ b/src/Lean/MetavarContext.lean
@@ -895,7 +895,7 @@ mutual
           let newLocalInsts := mvarDecl.localInstances.filter fun inst => toRevert.all fun x => inst.fvar != x
           -- Remark: we must reset the before processing `mkAuxMVarType` because `toRevert` may not be equal to `xs`
           let newMVarType ← withFreshCache do mkAuxMVarType mvarLCtx toRevert newMVarKind mvarDecl.type
-          let newMVarId ← get >>= fun s => pure s.ngen.curr
+          let newMVarId    := (← get).ngen.curr
           let newMVar      := mkMVar newMVarId
           let result       := mkMVarApp mvarLCtx newMVar toRevert newMVarKind
           let numScopeArgs := mvarDecl.numScopeArgs + result.getAppNumArgs