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 =>