diff --git a/src/Lean/Compiler/Old.lean b/src/Lean/Compiler/Old.lean
index 52908bc84eda..66f79ad1a2e3 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