From 8f59d4a9e65462cddacf3a56eddd963bbce40d41 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 16 Jan 2020 20:09:27 -0800
Subject: [PATCH] fix: `assignDelayed` misuse at `intro`

---
 src/Init/Lean/Meta/Tactic/Intro.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/Init/Lean/Meta/Tactic/Intro.lean b/src/Init/Lean/Meta/Tactic/Intro.lean
index e5262f3e94..220fb7d922 100644
--- a/src/Init/Lean/Meta/Tactic/Intro.lean
+++ b/src/Init/Lean/Meta/Tactic/Intro.lean
@@ -18,7 +18,8 @@ def introNCoreAux {σ} (mvarId : MVarId) (mkName : LocalContext → Name → σ
     withNewLocalInstances isClassExpensive fvars j $ do
       newMVar ← mkFreshExprSyntheticOpaqueMVar type;
       lctx    ← getLCtx;
-      modify $ fun s => { mctx := s.mctx.assignDelayed mvarId lctx fvars newMVar, .. s };
+      newVal  ← mkLambda fvars newMVar;
+      modify $ fun s => { mctx := s.mctx.assignExpr mvarId newVal, .. s };
       pure $ (fvars, newMVar.mvarId!)
 | (i+1), lctx, fvars, j, s, Expr.letE n type val body _ => do
   let type   := type.instantiateRevRange j fvars.size fvars;