From 212456720cb1982233d705ccee034351e80fbd90 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Aug 2022 10:15:43 -0700
Subject: [PATCH] fix: bug at `TerminalCases`

`Context.jp?` is not a continuation for the local lambda.
---
 src/Lean/Compiler/TerminalCases.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Compiler/TerminalCases.lean b/src/Lean/Compiler/TerminalCases.lean
index 99fea4d97a..5d3b47763c 100644
--- a/src/Lean/Compiler/TerminalCases.lean
+++ b/src/Lean/Compiler/TerminalCases.lean
@@ -55,7 +55,7 @@ partial def visitLet (e : Expr) (fvars : Array Expr) : M Expr := do
         visitCases casesInfo value
     else
       if value.isLambda then
-        value ← visitLambda value
+        value ← withReader (fun _ => {}) <| visitLambda value
       let fvar ← mkLetDecl binderName type value nonDep
       visitLet body (fvars.push fvar)
   | e =>