diff --git a/src/Lean/AddDecl.lean b/src/Lean/AddDecl.lean
index 128fb20a00..08386f4c9b 100644
--- a/src/Lean/AddDecl.lean
+++ b/src/Lean/AddDecl.lean
@@ -21,11 +21,6 @@ def Environment.addDecl (env : Environment) (opts : Options) (decl : Declaration
   else
     addDeclCore env (Core.getMaxHeartbeats opts).toUSize decl cancelTk?
 
-def Environment.addAndCompile (env : Environment) (opts : Options) (decl : Declaration)
-    (cancelTk? : Option IO.CancelToken := none) : Except KernelException Environment := do
-  let env ← addDecl env opts decl cancelTk?
-  compileDecl env opts decl
-
 def addDecl (decl : Declaration) : CoreM Unit := do
   profileitM Exception "type checking" (← getOptions) do
     withTraceNode `Kernel (fun _ => return m!"typechecking declaration") do
diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean
index 212e3c6de3..ce27e263d3 100644
--- a/src/Lean/Compiler/InitAttr.lean
+++ b/src/Lean/Compiler/InitAttr.lean
@@ -144,11 +144,7 @@ def declareBuiltin (forDecl : Name) (value : Expr) : CoreM Unit := do
   let type := mkApp (mkConst `IO) (mkConst `Unit)
   let decl := Declaration.defnDecl { name, levelParams := [], type, value, hints := ReducibilityHints.opaque,
                                      safety := DefinitionSafety.safe }
-  match (← getEnv).addAndCompile {} decl with
-  -- TODO: pretty print error
-  | Except.error e => do
-    let msg ← (e.toMessageData {}).toString
-    throwError "failed to emit registration code for builtin '{forDecl}': {msg}"
-  | Except.ok env  => IO.ofExcept (setBuiltinInitAttr env name) >>= setEnv
+  addAndCompile decl
+  IO.ofExcept (setBuiltinInitAttr (← getEnv) name) >>= setEnv
 
 end Lean
diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean
index 52908bc84e..66f79ad1a2 100644
--- a/src/Lean/Compiler/Old.lean
+++ b/src/Lean/Compiler/Old.lean
@@ -53,18 +53,3 @@ def isUnsafeRecName? : Name → Option Name
   | _ => none
 
 end Compiler
-
-namespace Environment
-
-/--
-Compile the given block of mutual declarations.
-Assumes the declarations have already been added to the environment using `addDecl`.
--/
-@[extern "lean_compile_decls"]
-opaque compileDecls (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
-
-/-- Compile the given declaration, it assumes the declaration has already been added to the environment using `addDecl`. -/
-def compileDecl (env : Environment) (opt : @& Options) (decl : @& Declaration) : Except KernelException Environment :=
-  compileDecls env opt (Compiler.getDeclNamesForCodeGen decl)
-
-end Environment
diff --git a/src/Lean/CoreM.lean b/src/Lean/CoreM.lean
index f6d34ca804..d541bb1951 100644
--- a/src/Lean/CoreM.lean
+++ b/src/Lean/CoreM.lean
@@ -514,13 +514,16 @@ register_builtin_option compiler.enableNew : Bool := {
 @[extern "lean_lcnf_compile_decls"]
 opaque compileDeclsNew (declNames : List Name) : CoreM Unit
 
+@[extern "lean_compile_decls"]
+opaque compileDeclsOld (env : Environment) (opt : @& Options) (decls : @& List Name) : Except KernelException Environment
+
 def compileDecl (decl : Declaration) : CoreM Unit := do
   let opts ← getOptions
   let decls := Compiler.getDeclNamesForCodeGen decl
   if compiler.enableNew.get opts then
     compileDeclsNew decls
   let res ← withTraceNode `compiler (fun _ => return m!"compiling old: {decls}") do
-    return (← getEnv).compileDecl opts decl
+    return compileDeclsOld (← getEnv) opts decls
   match res with
   | Except.ok env => setEnv env
   | Except.error (KernelException.other msg) =>
@@ -533,7 +536,7 @@ def compileDecls (decls : List Name) : CoreM Unit := do
   let opts ← getOptions
   if compiler.enableNew.get opts then
     compileDeclsNew decls
-  match (← getEnv).compileDecls opts decls with
+  match compileDeclsOld (← getEnv) opts decls with
   | Except.ok env   => setEnv env
   | Except.error (KernelException.other msg) =>
     throwError msg
diff --git a/src/Lean/ParserCompiler.lean b/src/Lean/ParserCompiler.lean
index 3d15ea6436..6cdc9ce46a 100644
--- a/src/Lean/ParserCompiler.lean
+++ b/src/Lean/ParserCompiler.lean
@@ -103,11 +103,8 @@ partial def compileParserExpr (e : Expr) : MetaM Expr := do
           name := c', levelParams := []
           type := ty, value := value, hints := ReducibilityHints.opaque, safety := DefinitionSafety.safe
         }
-        let env ← getEnv
-        let env ← match env.addAndCompile {} decl with
-          | Except.ok    env => pure env
-          | Except.error kex => do throwError (← (kex.toMessageData {}).toString)
-        setEnv <| ctx.combinatorAttr.setDeclFor env c c'
+        addAndCompile decl
+        modifyEnv (ctx.combinatorAttr.setDeclFor · c c')
         if cinfo.type.isConst then
           if let some kind ← parserNodeKind? cinfo.value! then
             -- If the parser is parameter-less and produces a node of kind `kind`,
diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean
index e44c93603a..6131320902 100644
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@@ -14,16 +14,17 @@ let decl := Declaration.defnDecl {
   safety      := DefinitionSafety.safe
 };
 IO.println (toExpr a);
-(match env.addAndCompile {} decl with
-| Except.error _ => throwError "addDecl failed"
-| Except.ok env  =>
-  match env.evalConst α {} auxName with
-  | Except.error ex => throwError ex
-  | Except.ok b => do
-    IO.println b;
-    unless a == b do
-      throwError "toExpr failed";
-    pure ())
+let oldEnv ← getEnv;
+addAndCompile decl;
+let newEnv ← getEnv
+setEnv oldEnv
+match newEnv.evalConst α {} auxName with
+| Except.error ex => throwError ex
+| Except.ok b => do
+  IO.println b;
+  unless a == b do
+    throwError "toExpr failed";
+  pure ()
 
 #eval test #[(1, 2), (3, 4)]
 #eval test ['a', 'b', 'c']