diff --git a/src/Lean/Compiler/LCNF/ToLCNF.lean b/src/Lean/Compiler/LCNF/ToLCNF.lean index 84f78e080a..cd13425a9c 100644 --- a/src/Lean/Compiler/LCNF/ToLCNF.lean +++ b/src/Lean/Compiler/LCNF/ToLCNF.lean @@ -714,7 +714,7 @@ where return .fvar funDecl.fvarId visitMData (mdata : MData) (e : Expr) : M Expr := do - if let some (.app (.lam n t b ..) v) := letFunAnnotation? e then + if let some (.app (.lam n t b ..) v) := letFunAnnotation? (.mdata mdata e) then visitLet (.letE n t v b (nonDep := true)) #[] else if isCompilerRelevantMData mdata then mkAuxLetDecl <| .mdata mdata (← visit e)