diff --git a/src/Lean/Compiler/LCNF/Simp/Main.lean b/src/Lean/Compiler/LCNF/Simp/Main.lean index c88d905a20..50e43769ae 100644 --- a/src/Lean/Compiler/LCNF/Simp/Main.lean +++ b/src/Lean/Compiler/LCNF/Simp/Main.lean @@ -223,7 +223,6 @@ partial def simp (code : Code) : SimpM Code := withIncRecDepth do let mut decl ← normLetDecl baseDecl if baseDecl != decl then markSimplified - if let some value ← simpValue? decl.value then markSimplified decl ← decl.updateValue value