diff --git a/src/Lean/Elab/Import.lean b/src/Lean/Elab/Import.lean
index d3fe944fbd..a5eb91be3c 100644
--- a/src/Lean/Elab/Import.lean
+++ b/src/Lean/Elab/Import.lean
@@ -1,10 +1,10 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura, Sebastian Ullrich
 -/
 import Lean.Parser.Module
-new_frontend
 namespace Lean.Elab
 
 def headerToImports (header : Syntax) : List Import :=
diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean
index 405cf6c9c7..60e2c3f7fc 100644
--- a/src/Lean/Elab/LetRec.lean
+++ b/src/Lean/Elab/LetRec.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2020 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -7,7 +8,6 @@ import Lean.Elab.Attributes
 import Lean.Elab.Binders
 import Lean.Elab.DeclModifiers
 import Lean.Elab.SyntheticMVars
-new_frontend
 namespace Lean.Elab.Term
 open Meta
 
diff --git a/src/Lean/Elab/Level.lean b/src/Lean/Elab/Level.lean
index 6186ed7691..9f36843434 100644
--- a/src/Lean/Elab/Level.lean
+++ b/src/Lean/Elab/Level.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -6,7 +7,6 @@ Authors: Leonardo de Moura
 import Lean.Meta.LevelDefEq
 import Lean.Elab.Exception
 import Lean.Elab.Log
-new_frontend
 
 namespace Lean.Elab.Level
 
diff --git a/src/Lean/Elab/Log.lean b/src/Lean/Elab/Log.lean
index 1d85b8c673..295665b878 100644
--- a/src/Lean/Elab/Log.lean
+++ b/src/Lean/Elab/Log.lean
@@ -1,3 +1,4 @@
+#lang lean4
 /-
 Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -5,7 +6,6 @@ Authors: Leonardo de Moura
 -/
 import Lean.Elab.Util
 import Lean.Elab.Exception
-new_frontend
 
 namespace Lean.Elab