From 32f219772c07b36d30bf435dbf3c91f9d18e9f8b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 29 Jan 2021 12:39:13 -0800
Subject: [PATCH] chore: minor

---
 src/Lean/MetavarContext.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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