diff --git a/src/Lean/Compiler/LCNF/Main.lean b/src/Lean/Compiler/LCNF/Main.lean
index 8a8171e93b..45e217882e 100644
--- a/src/Lean/Compiler/LCNF/Main.lean
+++ b/src/Lean/Compiler/LCNF/Main.lean
@@ -76,7 +76,9 @@ def run (declNames : Array Name) : CompilerM (Array Decl) := withAtLeastMaxRecDe
     withPhase pass.phase <| checkpoint pass.name decls
   if (← Lean.isTracingEnabledFor `Compiler.result) then
     for decl in decls do
-      Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl decl}"
+      -- We display the declaration saved in the environment because the names have been normalized
+      let some decl' ← getDeclAt? decl.name .base | unreachable!
+      Lean.addTrace `Compiler.result m!"size: {decl.size}\n{← ppDecl' decl'}"
   return decls
 
 end PassManager
diff --git a/src/Lean/Compiler/LCNF/PhaseExt.lean b/src/Lean/Compiler/LCNF/PhaseExt.lean
index 9fefc2902b..744d2dbc11 100644
--- a/src/Lean/Compiler/LCNF/PhaseExt.lean
+++ b/src/Lean/Compiler/LCNF/PhaseExt.lean
@@ -54,8 +54,16 @@ def getDeclAt? (declName : Name) (phase : Phase) : CoreM (Option Decl) :=
 def getDecl? (declName : Name) : CompilerM (Option Decl) := do
   getDeclAt? declName (← getPhase)
 
+def normalizeFVarIds (decl : Decl) : CoreM Decl := do
+  let ngenSaved ← getNGen
+  setNGen {}
+  try
+    CompilerM.run <| decl.internalize
+  finally
+    setNGen ngenSaved
+
 def saveBase : Pass :=
-  .mkPerDeclaration `saveBase (fun decl => do decl.saveBase; return decl) .base
+  .mkPerDeclaration `saveBase (fun decl => do (← normalizeFVarIds decl).saveBase; return decl) .base
 
 def forEachDecl (f : Decl → CoreM Unit) : CoreM Unit := do
   let env ← getEnv