diff --git a/src/Lean/Compiler/LCNF.lean b/src/Lean/Compiler/LCNF.lean
index dc8ed5af6f..e69c59f75f 100644
--- a/src/Lean/Compiler/LCNF.lean
+++ b/src/Lean/Compiler/LCNF.lean
@@ -35,4 +35,5 @@ import Lean.Compiler.LCNF.Types
 import Lean.Compiler.LCNF.Util
 import Lean.Compiler.LCNF.ConfigOptions
 import Lean.Compiler.LCNF.ForEachExpr
-import Lean.Compiler.LCNF.MonoTypes
\ No newline at end of file
+import Lean.Compiler.LCNF.MonoTypes
+import Lean.Compiler.LCNF.ToMono
\ No newline at end of file
diff --git a/src/Lean/Compiler/LCNF/ToMono.lean b/src/Lean/Compiler/LCNF/ToMono.lean
index 5ea1efb0b9..29a524bbab 100644
--- a/src/Lean/Compiler/LCNF/ToMono.lean
+++ b/src/Lean/Compiler/LCNF/ToMono.lean
@@ -62,6 +62,16 @@ def Decl.toMono (decl : Decl) : CompilerM Decl := do
   let type ← toMonoType decl.type
   let params ← decl.params.mapM (·.toMono)
   let value ← decl.value.toMono
-  return { decl with type, params, value, levelParams := [] }
+  let decl := { decl with type, params, value, levelParams := [] }
+  decl.saveMono
+  return decl
+
+def toMono : Pass where
+  name  := `toMono
+  run   := fun decls => decls.mapM (·.toMono)
+  phase := .base
+
+builtin_initialize
+  registerTraceClass `Compiler.toMono (inherited := true)
 
 end Lean.Compiler.LCNF
\ No newline at end of file