diff --git a/src/Lean/Compiler/LCNF/ExtractClosed.lean b/src/Lean/Compiler/LCNF/ExtractClosed.lean index 80b766cef1..1ef4044c95 100644 --- a/src/Lean/Compiler/LCNF/ExtractClosed.lean +++ b/src/Lean/Compiler/LCNF/ExtractClosed.lean @@ -111,7 +111,7 @@ partial def visitCode (code : Code) : M Code := do eraseCode closedCode pure closedTermName else - let name := (← read).baseName ++ (`_closedTerm).appendIndexAfter (← get).decls.size + let name := (← read).baseName ++ (`_closed).appendIndexAfter (← get).decls.size cacheClosedTermName env closedExpr name |> setEnv let decl := { name, levelParams := [], type := decl.type, params := #[], value := .code closedCode, inlineAttr? := some .noinline }