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