diff --git a/tests/compiler/append.lean b/tests/compiler/append.lean
index 396c64cb2c..8e75182651 100644
--- a/tests/compiler/append.lean
+++ b/tests/compiler/append.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def main (xs : List String) : IO Unit :=
 let ys1 := List.replicate 1000000 1;
diff --git a/tests/compiler/array_test.lean b/tests/compiler/array_test.lean
index 54b4660905..1eaa97b82b 100644
--- a/tests/compiler/array_test.lean
+++ b/tests/compiler/array_test.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo (a : Array Nat) : Array Nat :=
 let a := a.push 0
diff --git a/tests/compiler/binomial.lean b/tests/compiler/binomial.lean
index c5bb24db8c..2dc8a77d86 100644
--- a/tests/compiler/binomial.lean
+++ b/tests/compiler/binomial.lean
@@ -1,5 +1,5 @@
 import Std.Data.BinomialHeap
-new_frontend
+
 open Std
 
 abbrev Heap := BinomialHeap Nat (fun a b => a < b)
diff --git a/tests/compiler/bytearray_bug.lean b/tests/compiler/bytearray_bug.lean
index ca713b20ac..69cace5119 100644
--- a/tests/compiler/bytearray_bug.lean
+++ b/tests/compiler/bytearray_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def main (xs : List String) : IO Unit :=
   let arr := (let e := ByteArray.empty; e.push (UInt8.ofNat 10));
   let v := arr.data.get! 0;
diff --git a/tests/compiler/closure_bug1.lean b/tests/compiler/closure_bug1.lean
index b1d387f975..9e7783ee6a 100644
--- a/tests/compiler/closure_bug1.lean
+++ b/tests/compiler/closure_bug1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2
diff --git a/tests/compiler/closure_bug2.lean b/tests/compiler/closure_bug2.lean
index 56ecba0862..ca586cfb30 100644
--- a/tests/compiler/closure_bug2.lean
+++ b/tests/compiler/closure_bug2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2
diff --git a/tests/compiler/closure_bug3.lean b/tests/compiler/closure_bug3.lean
index 4300073107..5b9c17daf6 100644
--- a/tests/compiler/closure_bug3.lean
+++ b/tests/compiler/closure_bug3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2
diff --git a/tests/compiler/closure_bug4.lean b/tests/compiler/closure_bug4.lean
index 7f3e3e2b8c..3bd1dff6db 100644
--- a/tests/compiler/closure_bug4.lean
+++ b/tests/compiler/closure_bug4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1
 let x2 := x + 2
diff --git a/tests/compiler/closure_bug5.lean b/tests/compiler/closure_bug5.lean
index d623bb45e6..1690d3d1be 100644
--- a/tests/compiler/closure_bug5.lean
+++ b/tests/compiler/closure_bug5.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;
diff --git a/tests/compiler/closure_bug6.lean b/tests/compiler/closure_bug6.lean
index c5f1041eaf..22a55348e0 100644
--- a/tests/compiler/closure_bug6.lean
+++ b/tests/compiler/closure_bug6.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;
diff --git a/tests/compiler/closure_bug7.lean b/tests/compiler/closure_bug7.lean
index 50cfb4d13f..48bb9627b4 100644
--- a/tests/compiler/closure_bug7.lean
+++ b/tests/compiler/closure_bug7.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;
diff --git a/tests/compiler/closure_bug8.lean b/tests/compiler/closure_bug8.lean
index 715dc3901e..a8b38a0419 100644
--- a/tests/compiler/closure_bug8.lean
+++ b/tests/compiler/closure_bug8.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) : Nat × (Nat → String) :=
 let x1 := x + 1;
 let x2 := x + 2;
diff --git a/tests/compiler/expr.lean b/tests/compiler/expr.lean
index 2852d74558..e6f5896e92 100644
--- a/tests/compiler/expr.lean
+++ b/tests/compiler/expr.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 def main : IO UInt32 := do
diff --git a/tests/compiler/float.lean b/tests/compiler/float.lean
index 014ba0b630..ae2e98122a 100644
--- a/tests/compiler/float.lean
+++ b/tests/compiler/float.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def tst1 : IO Unit := do
 IO.println (1 : Float);
 IO.println ((1 : Float) + 2);
diff --git a/tests/compiler/float_cases_bug.lean b/tests/compiler/float_cases_bug.lean
index ffa44325fb..e789988e21 100644
--- a/tests/compiler/float_cases_bug.lean
+++ b/tests/compiler/float_cases_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 inductive Term : Type
 | const : Nat -> Term
 | app   : List Term -> Term
diff --git a/tests/compiler/init.lean b/tests/compiler/init.lean
index 66bc172bee..e83f7f519a 100644
--- a/tests/compiler/init.lean
+++ b/tests/compiler/init.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 
diff --git a/tests/compiler/lazylist.lean b/tests/compiler/lazylist.lean
index 33730b802c..753fb0d04c 100644
--- a/tests/compiler/lazylist.lean
+++ b/tests/compiler/lazylist.lean
@@ -3,7 +3,7 @@ Copyright (c) 2019 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 -/
-new_frontend
+
 universes u v w
 
 inductive LazyList (α : Type u)
diff --git a/tests/compiler/map_big.lean b/tests/compiler/map_big.lean
index a0413990b4..5b35263d00 100644
--- a/tests/compiler/map_big.lean
+++ b/tests/compiler/map_big.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f2 (n : Nat) (xs : List Nat) : List (List Nat) :=
 let ys := List.replicate n 0;
 xs.map (fun x => x :: ys)
diff --git a/tests/compiler/partial.lean b/tests/compiler/partial.lean
index a7b90b22d3..aeef0db262 100644
--- a/tests/compiler/partial.lean
+++ b/tests/compiler/partial.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 set_option pp.implicit true
 set_option pp.binder_types false
 -- set_option trace.compiler.boxed true
diff --git a/tests/compiler/phashmap.lean b/tests/compiler/phashmap.lean
index 79c7fd7863..e745908a51 100644
--- a/tests/compiler/phashmap.lean
+++ b/tests/compiler/phashmap.lean
@@ -1,6 +1,6 @@
 import Std.Data.PersistentHashMap
 import Lean.Data.Format
-new_frontend
+
 open Lean Std Std.PersistentHashMap
 
 abbrev Map := PersistentHashMap Nat Nat
diff --git a/tests/elabissues/invalid_field_notation_error_msg.lean b/tests/elabissues/invalid_field_notation_error_msg.lean
index ca83821d81..fa3293593a 100644
--- a/tests/elabissues/invalid_field_notation_error_msg.lean
+++ b/tests/elabissues/invalid_field_notation_error_msg.lean
@@ -15,7 +15,7 @@ def Foo.f3 (f : Foo) : Nat := f.n
 def Foo.f4 (f : Foo) : Nat := f.n
 def Foo.f5 (f : Foo) : Nat := f.n
 
-new_frontend
+
 
 #check (λ f g h =>
   let x : Foo := ⟨f.n + 1⟩;
diff --git a/tests/lean/IRbug.lean b/tests/lean/IRbug.lean
index 8adc37f9fe..5b291b4901 100644
--- a/tests/lean/IRbug.lean
+++ b/tests/lean/IRbug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Repro
 
diff --git a/tests/lean/PPRoundtrip.lean b/tests/lean/PPRoundtrip.lean
index 7677bc324c..d98a5a4acf 100644
--- a/tests/lean/PPRoundtrip.lean
+++ b/tests/lean/PPRoundtrip.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 open Lean.Elab
 open Lean.Elab.Term
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
index aa9721ec8b..425e86fe39 100644
--- a/tests/lean/Process.lean
+++ b/tests/lean/Process.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 open IO.Process
 
 def usingIO {α} (x : IO α) : IO α := x
diff --git a/tests/lean/Reformat.lean b/tests/lean/Reformat.lean
index 78b12a3b6f..dd9879a8b3 100644
--- a/tests/lean/Reformat.lean
+++ b/tests/lean/Reformat.lean
@@ -1,6 +1,6 @@
 /-! Parse and reformat file -/
 import Lean.PrettyPrinter
-new_frontend
+
 open Lean
 open Lean.Elab
 open Lean.Elab.Term
diff --git a/tests/lean/StxQuot.lean b/tests/lean/StxQuot.lean
index 77e9993b56..48d19eca4c 100644
--- a/tests/lean/StxQuot.lean
+++ b/tests/lean/StxQuot.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 namespace Lean
 open Lean.Elab
 
diff --git a/tests/lean/abst.lean b/tests/lean/abst.lean
index e355e3809c..c7689a15c1 100644
--- a/tests/lean/abst.lean
+++ b/tests/lean/abst.lean
@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def tst : IO Unit :=
diff --git a/tests/lean/appParserIssue.lean b/tests/lean/appParserIssue.lean
index c616cacc72..d80c2582ac 100644
--- a/tests/lean/appParserIssue.lean
+++ b/tests/lean/appParserIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (x : Nat) (g : Nat → Nat) := g x
 
 #check f 1 fun x => x   -- should work
diff --git a/tests/lean/attrCmd.lean b/tests/lean/attrCmd.lean
index ad7f4d7bcd..d3613697df 100644
--- a/tests/lean/attrCmd.lean
+++ b/tests/lean/attrCmd.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def M := StateM Nat
 
diff --git a/tests/lean/auxDeclIssue.lean b/tests/lean/auxDeclIssue.lean
index 63a08d00b9..1d4b3484b1 100644
--- a/tests/lean/auxDeclIssue.lean
+++ b/tests/lean/auxDeclIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem ex1 : False :=
 by {
diff --git a/tests/lean/binsearch.lean b/tests/lean/binsearch.lean
index a3a411edc2..b4b41f0cf0 100644
--- a/tests/lean/binsearch.lean
+++ b/tests/lean/binsearch.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 partial def mkAssocArray : Nat → Array (Nat × Bool) → Array (Nat × Bool)
 | 0,   as => as
 | i+1, as  => mkAssocArray i (as.push (i, i % 2 == 0))
diff --git a/tests/lean/bytearray.lean b/tests/lean/bytearray.lean
index 966ae61397..41aed42023 100644
--- a/tests/lean/bytearray.lean
+++ b/tests/lean/bytearray.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def tst : IO Unit :=
 do
 let bs := [1, 2, 3].toByteArray;
diff --git a/tests/lean/classBadOutParam.lean b/tests/lean/classBadOutParam.lean
index 2ffb6389de..5f3b9c7250 100644
--- a/tests/lean/classBadOutParam.lean
+++ b/tests/lean/classBadOutParam.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 class C1 (x : outParam Nat) (y : { n : Nat // n > x }) (α : Type) := -- should fail
 (val : α)
 
diff --git a/tests/lean/collectDepsIssue.lean b/tests/lean/collectDepsIssue.lean
index bea5af6cab..349f2244fc 100644
--- a/tests/lean/collectDepsIssue.lean
+++ b/tests/lean/collectDepsIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 variables {α : Type} in
 def f (a : α) : List α :=
diff --git a/tests/lean/ctor_layout.lean b/tests/lean/ctor_layout.lean
index dad9f5ffcb..9bc09cce05 100644
--- a/tests/lean/ctor_layout.lean
+++ b/tests/lean/ctor_layout.lean
@@ -1,5 +1,5 @@
 import Lean.Compiler.IR
-new_frontend
+
 open Lean
 open Lean.IR
 
diff --git a/tests/lean/dbgMacros.lean b/tests/lean/dbgMacros.lean
index 05f2010673..6ffed96002 100644
--- a/tests/lean/dbgMacros.lean
+++ b/tests/lean/dbgMacros.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) :=
 if x = 0 then panic! "unexpected zero"
diff --git a/tests/lean/doNotation1.lean b/tests/lean/doNotation1.lean
index 24d6f52b4d..879062b61a 100644
--- a/tests/lean/doNotation1.lean
+++ b/tests/lean/doNotation1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 (x : Nat) : IO Nat := do
 y := 1  -- error 'y' cannot be reassigned
diff --git a/tests/lean/doSeqRightIssue.lean b/tests/lean/doSeqRightIssue.lean
index f39a9598dd..497f747d9d 100644
--- a/tests/lean/doSeqRightIssue.lean
+++ b/tests/lean/doSeqRightIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u
 variables {α : Type u}
diff --git a/tests/lean/emptyc.lean b/tests/lean/emptyc.lean
index 5ad95b8468..766908074a 100644
--- a/tests/lean/emptyc.lean
+++ b/tests/lean/emptyc.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure A :=
 (x : Nat := 0)
diff --git a/tests/lean/evalWithMVar.lean b/tests/lean/evalWithMVar.lean
index e6795fa549..04d4a7131b 100644
--- a/tests/lean/evalWithMVar.lean
+++ b/tests/lean/evalWithMVar.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def c {α} : Sum α Nat :=
 Sum.inr 10
diff --git a/tests/lean/eval_except.lean b/tests/lean/eval_except.lean
index e5e2426bed..47daeb7013 100644
--- a/tests/lean/eval_except.lean
+++ b/tests/lean/eval_except.lean
@@ -1,5 +1,5 @@
 prelude
 import Init.System.IO
-new_frontend
+
 #eval (throw $ IO.userError "this is my error" : IO Unit)
 #eval (throw $ IO.Error.noFileOrDirectory "file.ext" 31 "and details" : IO Unit)
diff --git a/tests/lean/exitAfterParseError.lean b/tests/lean/exitAfterParseError.lean
index 8e3bf2e8c4..4d139b075f 100644
--- a/tests/lean/exitAfterParseError.lean
+++ b/tests/lean/exitAfterParseError.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo 
 
diff --git a/tests/lean/extract.lean b/tests/lean/extract.lean
index 2756d01a75..3cf07ab7dd 100644
--- a/tests/lean/extract.lean
+++ b/tests/lean/extract.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 #eval "abc"
 
 /- some "a" -/
diff --git a/tests/lean/file_not_found.lean b/tests/lean/file_not_found.lean
index 5f43fe9a64..57794d42fe 100644
--- a/tests/lean/file_not_found.lean
+++ b/tests/lean/file_not_found.lean
@@ -1,6 +1,6 @@
 prelude
 import Init.System.IO
-new_frontend
+
 open IO.FS
 def usingIO {α} (x : IO α) : IO α := x
 #eval (discard $ IO.FS.Handle.mk "non-existent-file.txt" Mode.read : IO Unit)
diff --git a/tests/lean/holeErrors.lean b/tests/lean/holeErrors.lean
index 9f56ae5d6e..d6be4d7452 100644
--- a/tests/lean/holeErrors.lean
+++ b/tests/lean/holeErrors.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 := id
 
diff --git a/tests/lean/holes.lean b/tests/lean/holes.lean
index ac72e420ad..9e6249a2c7 100644
--- a/tests/lean/holes.lean
+++ b/tests/lean/holes.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : Nat :=
 id (_ x)
diff --git a/tests/lean/hygienicIntro.lean b/tests/lean/hygienicIntro.lean
index dc6c533dfd..7acfda4124 100644
--- a/tests/lean/hygienicIntro.lean
+++ b/tests/lean/hygienicIntro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 set_option hygienicIntro false in
 theorem ex1 {a p q r : Prop} : p → (p → q) → (q → r) → r := by
diff --git a/tests/lean/inductive1.lean b/tests/lean/inductive1.lean
index c368c6d88c..9237910e4e 100644
--- a/tests/lean/inductive1.lean
+++ b/tests/lean/inductive1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- Test1
 inductive T1 : Nat -- Error, resultant type is not a sort
diff --git a/tests/lean/infoFromFailure.lean b/tests/lean/infoFromFailure.lean
index 04a0c1b1ba..b9c0b0f999 100644
--- a/tests/lean/infoFromFailure.lean
+++ b/tests/lean/infoFromFailure.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def A.foo {α : Type} [HasAdd α] (a : α) : α × α :=
 (a, a + a)
diff --git a/tests/lean/inst.lean b/tests/lean/inst.lean
index 37cd398715..f8970fa05c 100644
--- a/tests/lean/inst.lean
+++ b/tests/lean/inst.lean
@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def tst : IO Unit :=
diff --git a/tests/lean/json.lean b/tests/lean/json.lean
index 82296ad5e5..808237893b 100644
--- a/tests/lean/json.lean
+++ b/tests/lean/json.lean
@@ -1,6 +1,6 @@
 import Lean.Data.Json.Parser
 import Lean.Data.Json.Printer
-new_frontend
+
 def test (s : String) : String :=
 match Lean.Json.parse s with
 | Except.ok res    => toString res
diff --git a/tests/lean/letrec1.lean b/tests/lean/letrec1.lean
index 006b3c6acb..440f382af6 100644
--- a/tests/lean/letrec1.lean
+++ b/tests/lean/letrec1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1.g := 10
 
diff --git a/tests/lean/ll_infer_type_bug.lean b/tests/lean/ll_infer_type_bug.lean
index 4d148f5fdd..a71ae60d60 100644
--- a/tests/lean/ll_infer_type_bug.lean
+++ b/tests/lean/ll_infer_type_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 partial def f : List Nat → Bool
 | []      => false
 | (a::as) => a > 0 && f as
diff --git a/tests/lean/lvl1.lean b/tests/lean/lvl1.lean
index b4ed09fc87..0228d2673f 100644
--- a/tests/lean/lvl1.lean
+++ b/tests/lean/lvl1.lean
@@ -1,5 +1,5 @@
 import Lean.Level
-new_frontend
+
 namespace Lean
 namespace Level
 
diff --git a/tests/lean/macroStack.lean b/tests/lean/macroStack.lean
index 081f15317d..5480a9390d 100644
--- a/tests/lean/macroStack.lean
+++ b/tests/lean/macroStack.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 :=
 if h:x then 1 else 0
diff --git a/tests/lean/macroscopes.lean b/tests/lean/macroscopes.lean
index 37ea91c864..eaee36cc93 100644
--- a/tests/lean/macroscopes.lean
+++ b/tests/lean/macroscopes.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 open Lean
 def check (b : Bool) : IO Unit :=
 «unless» b $ throw $ IO.userError "check failed"
diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean
index 24711c904d..889efa5ba9 100644
--- a/tests/lean/match1.lean
+++ b/tests/lean/match1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #print "---- h1"
 
diff --git a/tests/lean/match2.lean b/tests/lean/match2.lean
index 93d3936827..e171048bbb 100644
--- a/tests/lean/match2.lean
+++ b/tests/lean/match2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #print "---- Op"
 
diff --git a/tests/lean/match3.lean b/tests/lean/match3.lean
index 6f1fc3f0c7..38f35af958 100644
--- a/tests/lean/match3.lean
+++ b/tests/lean/match3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : Nat :=
 match x with
diff --git a/tests/lean/match4.lean b/tests/lean/match4.lean
index 8ce3060fb9..9026e68e2e 100644
--- a/tests/lean/match4.lean
+++ b/tests/lean/match4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 (x : Nat × Nat) : Nat :=
 match x with
diff --git a/tests/lean/matchErrorLocation.lean b/tests/lean/matchErrorLocation.lean
index f188cbff11..671b9c1047 100644
--- a/tests/lean/matchErrorLocation.lean
+++ b/tests/lean/matchErrorLocation.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def head {α} (xs : List α) (h : xs = [] → False) : α :=
 match he:xs with
diff --git a/tests/lean/mutualWithNamespaceMacro.lean b/tests/lean/mutualWithNamespaceMacro.lean
index 3d87549a7f..a00309b6be 100644
--- a/tests/lean/mutualWithNamespaceMacro.lean
+++ b/tests/lean/mutualWithNamespaceMacro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 mutual
 
diff --git a/tests/lean/mutualdef1.lean b/tests/lean/mutualdef1.lean
index 131073a388..fccf316c0f 100644
--- a/tests/lean/mutualdef1.lean
+++ b/tests/lean/mutualdef1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 mutual
 
diff --git a/tests/lean/mvar1.lean b/tests/lean/mvar1.lean
index f79fe379e8..85b4340918 100644
--- a/tests/lean/mvar1.lean
+++ b/tests/lean/mvar1.lean
@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def check (b : Bool) : IO Unit :=
diff --git a/tests/lean/mvar2.lean b/tests/lean/mvar2.lean
index 2465c8d5c2..43e7ac144f 100644
--- a/tests/lean/mvar2.lean
+++ b/tests/lean/mvar2.lean
@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def check (b : Bool) : IO Unit :=
diff --git a/tests/lean/mvar3.lean b/tests/lean/mvar3.lean
index 448f85ed4d..aa699db01b 100644
--- a/tests/lean/mvar3.lean
+++ b/tests/lean/mvar3.lean
@@ -1,5 +1,5 @@
 import Lean.MetavarContext
-new_frontend
+
 open Lean
 
 def mkLambdaTest (mctx : MetavarContext) (ngen : NameGenerator) (lctx : LocalContext) (xs : Array Expr) (e : Expr)
diff --git a/tests/lean/mvar_fvar.lean b/tests/lean/mvar_fvar.lean
index 04ad2435b5..0f7a2dc08e 100644
--- a/tests/lean/mvar_fvar.lean
+++ b/tests/lean/mvar_fvar.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 #eval (mkFVar `a).hasFVar
diff --git a/tests/lean/namedHoles.lean b/tests/lean/namedHoles.lean
index a9ee142f63..79269931a7 100644
--- a/tests/lean/namedHoles.lean
+++ b/tests/lean/namedHoles.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) (y : Bool) :=
 x + if y then 1 else 0
diff --git a/tests/lean/namelit.lean b/tests/lean/namelit.lean
index 1068ff04fb..f6ecef7e40 100644
--- a/tests/lean/namelit.lean
+++ b/tests/lean/namelit.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #check `foo
 #check `foo.bla
diff --git a/tests/lean/openExport.lean b/tests/lean/openExport.lean
index 85e3408921..e55c3b542a 100644
--- a/tests/lean/openExport.lean
+++ b/tests/lean/openExport.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def A.x := 10
 
diff --git a/tests/lean/parserPrio.lean b/tests/lean/parserPrio.lean
index 135d5b604a..60c052ad5e 100644
--- a/tests/lean/parserPrio.lean
+++ b/tests/lean/parserPrio.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- New notation that overlaps with existing notation
 syntax [myPair, 100] "(" term "," term ")" : term
diff --git a/tests/lean/phashmap_inst_coherence.lean b/tests/lean/phashmap_inst_coherence.lean
index 03d5a6c15d..0b4c5d5093 100644
--- a/tests/lean/phashmap_inst_coherence.lean
+++ b/tests/lean/phashmap_inst_coherence.lean
@@ -1,5 +1,5 @@
 import Std.Data.PersistentHashMap
-new_frontend
+
 open Std
 def m : PersistentHashMap Nat Nat :=
 let m : PersistentHashMap Nat Nat := {};
diff --git a/tests/lean/ppExpr.lean b/tests/lean/ppExpr.lean
index 48ee93061c..09f9ba0d68 100644
--- a/tests/lean/ppExpr.lean
+++ b/tests/lean/ppExpr.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 /-! Pretty printing tests for `Expr`s that cannot be generated by parsing+elaborating. -/
 
diff --git a/tests/lean/precissues.lean b/tests/lean/precissues.lean
index 5de542cb41..1dead871ae 100644
--- a/tests/lean/precissues.lean
+++ b/tests/lean/precissues.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #check id fun x => x -- should work
 
diff --git a/tests/lean/private.lean b/tests/lean/private.lean
index f12a0f88df..bd6aab1bf4 100644
--- a/tests/lean/private.lean
+++ b/tests/lean/private.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- Issue 1
 def foo := 10
diff --git a/tests/lean/protected.lean b/tests/lean/protected.lean
index 4765e3d389..a077fc3e33 100644
--- a/tests/lean/protected.lean
+++ b/tests/lean/protected.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 
diff --git a/tests/lean/ref1.lean b/tests/lean/ref1.lean
index b3f233f929..10035aced5 100644
--- a/tests/lean/ref1.lean
+++ b/tests/lean/ref1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def inc (r : IO.Ref Nat) : IO Unit := do
 let v ← r.get;
 r.set (v+1);
diff --git a/tests/lean/repr_issue.lean b/tests/lean/repr_issue.lean
index fd83f49aad..10f8f1808f 100644
--- a/tests/lean/repr_issue.lean
+++ b/tests/lean/repr_issue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def foo {m} [Monad m] [MonadExcept String m] [MonadState (Array Nat) m] : m Nat :=
 tryCatch
   (do modify $ fun (a : Array Nat) => a.set! 0 33;
diff --git a/tests/lean/resolveGlobalName.lean b/tests/lean/resolveGlobalName.lean
index 0113e21ed1..07fa54e1a8 100644
--- a/tests/lean/resolveGlobalName.lean
+++ b/tests/lean/resolveGlobalName.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 def Boo.x := 1
 def Foo.x := 2
diff --git a/tests/lean/rewrite.lean b/tests/lean/rewrite.lean
index 2d8d39568e..69798fb324 100644
--- a/tests/lean/rewrite.lean
+++ b/tests/lean/rewrite.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 axiom appendNil {α} (as : List α) : as ++ [] = as
 axiom appendAssoc {α} (as bs cs : List α) : (as ++ bs) ++ cs = as ++ (bs ++ cs)
diff --git a/tests/lean/run/108.lean b/tests/lean/run/108.lean
index 828b12a8ef..f07d647b03 100644
--- a/tests/lean/run/108.lean
+++ b/tests/lean/run/108.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro m n:ident : command => `(def $n := 1)
 
diff --git a/tests/lean/run/111.lean b/tests/lean/run/111.lean
index dc2a3636fa..35dae94fb9 100644
--- a/tests/lean/run/111.lean
+++ b/tests/lean/run/111.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 #check mkNullNode  -- Lean.Syntax
 #check mkNullNode #[]  -- Lean.Syntax
diff --git a/tests/lean/run/121.lean b/tests/lean/run/121.lean
index 792d867ad3..610c6e9bdf 100644
--- a/tests/lean/run/121.lean
+++ b/tests/lean/run/121.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev DelabM := Id
 abbrev Delab := DelabM Nat
diff --git a/tests/lean/run/125.lean b/tests/lean/run/125.lean
index 5191687e56..d54dc4d5d4 100644
--- a/tests/lean/run/125.lean
+++ b/tests/lean/run/125.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 class HasElems (α : Type) : Type := (elems : Array α)
 def elems (α : Type) [HasElems α] : Array α := HasElems.elems
diff --git a/tests/lean/run/175.lean b/tests/lean/run/175.lean
index 0b58912b95..b5353fb7a7 100644
--- a/tests/lean/run/175.lean
+++ b/tests/lean/run/175.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 namespace Foo
 open Lean.Elab.Term
diff --git a/tests/lean/run/1954.lean b/tests/lean/run/1954.lean
index 7cfe0f4371..ada449924d 100644
--- a/tests/lean/run/1954.lean
+++ b/tests/lean/run/1954.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def all (p : Nat → Prop) : Prop := ∀x, p x
 example {p : Nat → Prop} (h : all p) : p 0 := h 0
diff --git a/tests/lean/run/1968.lean b/tests/lean/run/1968.lean
index 1d4b53e6f1..702758f445 100644
--- a/tests/lean/run/1968.lean
+++ b/tests/lean/run/1968.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive type
 | bv  : Nat → type
diff --git a/tests/lean/run/28.lean b/tests/lean/run/28.lean
index fd11f21833..c300f19b0c 100644
--- a/tests/lean/run/28.lean
+++ b/tests/lean/run/28.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure bv (w : Nat) := (u:Unit)
 
diff --git a/tests/lean/run/29.lean b/tests/lean/run/29.lean
index 605f2ce0c4..a95ebdf91a 100644
--- a/tests/lean/run/29.lean
+++ b/tests/lean/run/29.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo : Nat -> Nat -> Nat -> List Nat
 | _, _, 0   => [1]
diff --git a/tests/lean/run/34.lean b/tests/lean/run/34.lean
index e2fd9519b5..f6ee81fd13 100644
--- a/tests/lean/run/34.lean
+++ b/tests/lean/run/34.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 partial def foo : ∀ (n : Nat), StateM Unit Unit
 | n =>
diff --git a/tests/lean/run/CoeNew.lean b/tests/lean/run/CoeNew.lean
index e23f909cf0..032140f73d 100644
--- a/tests/lean/run/CoeNew.lean
+++ b/tests/lean/run/CoeNew.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v w
 
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index 2e89f465b3..2a0476dac5 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax [mycheck] "#check" (sepBy term ",") : command
 
diff --git a/tests/lean/run/DefEqAssignBug.lean b/tests/lean/run/DefEqAssignBug.lean
index 85ded1d241..26b887e07b 100644
--- a/tests/lean/run/DefEqAssignBug.lean
+++ b/tests/lean/run/DefEqAssignBug.lean
@@ -1,6 +1,6 @@
 import Lean.Meta
 
-new_frontend
+
 
 open Lean
 open Lean.Meta
diff --git a/tests/lean/run/IO_test.lean b/tests/lean/run/IO_test.lean
index 0b784d2ed5..17f038babb 100644
--- a/tests/lean/run/IO_test.lean
+++ b/tests/lean/run/IO_test.lean
@@ -2,7 +2,7 @@ prelude
 import Init.System.IO
 import Init.Data.List.Control
 import Init.Data.ToString
-new_frontend
+
 
 open IO.FS
 
diff --git a/tests/lean/run/LiftMethodIssue.lean b/tests/lean/run/LiftMethodIssue.lean
index cd45420e79..bbc0b87109 100644
--- a/tests/lean/run/LiftMethodIssue.lean
+++ b/tests/lean/run/LiftMethodIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst : IO (Option Nat) := do
 let x? : Option Nat ← pure none;
diff --git a/tests/lean/run/Reid1.lean b/tests/lean/run/Reid1.lean
index a8f860b1eb..4d71c55276 100644
--- a/tests/lean/run/Reid1.lean
+++ b/tests/lean/run/Reid1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure ConstantFunction (α β : Type) :=
 (f : α → β)
diff --git a/tests/lean/run/Reparen.lean b/tests/lean/run/Reparen.lean
index 04234ee876..f5ceb4d97c 100644
--- a/tests/lean/run/Reparen.lean
+++ b/tests/lean/run/Reparen.lean
@@ -1,6 +1,6 @@
 /-! Reprint file after removing all parentheses and then passing it through the parenthesizer -/
 import Lean.Parser
-new_frontend
+
 open Lean
 open Lean.Format
 
diff --git a/tests/lean/run/anonymous_ctor_error_msg.lean b/tests/lean/run/anonymous_ctor_error_msg.lean
index 34725c28b7..916537c04c 100644
--- a/tests/lean/run/anonymous_ctor_error_msg.lean
+++ b/tests/lean/run/anonymous_ctor_error_msg.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure Foo := (n : Nat)
 
diff --git a/tests/lean/run/array1.lean b/tests/lean/run/array1.lean
index 246e3901c8..e46798992e 100644
--- a/tests/lean/run/array1.lean
+++ b/tests/lean/run/array1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 #check @Array.mk
 
 def v : Array Nat := @Array.mk Nat 10 (fun ⟨i, _⟩ => i)
diff --git a/tests/lean/run/autoparam.lean b/tests/lean/run/autoparam.lean
index 4e35e1296f..3aa2b5e82a 100644
--- a/tests/lean/run/autoparam.lean
+++ b/tests/lean/run/autoparam.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x y : Nat) (h : x = y := by assumption) : Nat :=
 x + x
diff --git a/tests/lean/run/backtrackable_estate.lean b/tests/lean/run/backtrackable_estate.lean
index 16c1365e37..4ab0fe01fd 100644
--- a/tests/lean/run/backtrackable_estate.lean
+++ b/tests/lean/run/backtrackable_estate.lean
@@ -1,5 +1,5 @@
 import Init.System.IO
-new_frontend
+
 
 structure MyState :=
 (bs : Nat := 0) -- backtrackable state
diff --git a/tests/lean/run/bigmul.lean b/tests/lean/run/bigmul.lean
index 52da5048cf..0f0ac3c8df 100644
--- a/tests/lean/run/bigmul.lean
+++ b/tests/lean/run/bigmul.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 @[noinline] def f (x : Nat) :=
 1000000000000000000000000000000
diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean
index 8c26950717..adde091f1a 100644
--- a/tests/lean/run/bigop.lean
+++ b/tests/lean/run/bigop.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def Seq (α : Type) := List α
 
diff --git a/tests/lean/run/borrowBug.lean b/tests/lean/run/borrowBug.lean
index 78724151b3..36869cbd1a 100644
--- a/tests/lean/run/borrowBug.lean
+++ b/tests/lean/run/borrowBug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 @[noinline] def g (x : Nat) : Nat × Nat := (x, x)
 @[noinline] def p (x : Nat) : Bool := x > 10
diff --git a/tests/lean/run/catchThe.lean b/tests/lean/run/catchThe.lean
index cb1c7113ee..6d4144f2be 100644
--- a/tests/lean/run/catchThe.lean
+++ b/tests/lean/run/catchThe.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/cdotTests.lean b/tests/lean/run/cdotTests.lean
index 084a35cfac..f75301a211 100644
--- a/tests/lean/run/cdotTests.lean
+++ b/tests/lean/run/cdotTests.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 class Inc (α : Type) :=
 (inc : α → α)
diff --git a/tests/lean/run/check.lean b/tests/lean/run/check.lean
index 6aea5e6171..e0db32605e 100644
--- a/tests/lean/run/check.lean
+++ b/tests/lean/run/check.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 --
 
 #check And.intro
diff --git a/tests/lean/run/choiceExpectedTypeBug.lean b/tests/lean/run/choiceExpectedTypeBug.lean
index 8286e58bfe..1137207df4 100644
--- a/tests/lean/run/choiceExpectedTypeBug.lean
+++ b/tests/lean/run/choiceExpectedTypeBug.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 structure A :=
 (x : Nat := 10)
diff --git a/tests/lean/run/choiceMacroRules.lean b/tests/lean/run/choiceMacroRules.lean
index d5a3ebf625..80708bc656 100644
--- a/tests/lean/run/choiceMacroRules.lean
+++ b/tests/lean/run/choiceMacroRules.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax:65 [myAdd1] term "+++" term:65 : term
 syntax:65 [myAdd2] term "+++" term:65 : term
diff --git a/tests/lean/run/closure1.lean b/tests/lean/run/closure1.lean
index 4b53efdf2a..c8d6f3ab88 100644
--- a/tests/lean/run/closure1.lean
+++ b/tests/lean/run/closure1.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/coeIssue1.lean b/tests/lean/run/coeIssue1.lean
index d57274c256..e9e4ea34fc 100644
--- a/tests/lean/run/coeIssue1.lean
+++ b/tests/lean/run/coeIssue1.lean
@@ -1,6 +1,6 @@
 -- From @joehendrix
 -- The imul doesn't type check as Lean won't try to coerce from a reg (bv 64) to a expr (bv ?u)
-new_frontend
+
 
 inductive MCType
 | bv : Nat → MCType
diff --git a/tests/lean/run/coeIssue2.lean b/tests/lean/run/coeIssue2.lean
index c0baca2ce2..87f9f73c55 100644
--- a/tests/lean/run/coeIssue2.lean
+++ b/tests/lean/run/coeIssue2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure A :=
 (a : Nat)
diff --git a/tests/lean/run/coeIssue3.lean b/tests/lean/run/coeIssue3.lean
index 3cd710985d..c84587b826 100644
--- a/tests/lean/run/coeIssue3.lean
+++ b/tests/lean/run/coeIssue3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure Var : Type := (name : String)
 instance Var.nameCoe : Coe String Var := ⟨Var.mk⟩
diff --git a/tests/lean/run/coeIssues4.lean b/tests/lean/run/coeIssues4.lean
index b1d1866e73..f96296207b 100644
--- a/tests/lean/run/coeIssues4.lean
+++ b/tests/lean/run/coeIssues4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f : List Int → Bool := fun _ => true
 
diff --git a/tests/lean/run/coeSort1.lean b/tests/lean/run/coeSort1.lean
index 715aadabad..0b68a869de 100644
--- a/tests/lean/run/coeSort1.lean
+++ b/tests/lean/run/coeSort1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u
 
diff --git a/tests/lean/run/coeSort2.lean b/tests/lean/run/coeSort2.lean
index 29452dd0c7..7948504179 100644
--- a/tests/lean/run/coeSort2.lean
+++ b/tests/lean/run/coeSort2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universe u
 
diff --git a/tests/lean/run/coelambda.lean b/tests/lean/run/coelambda.lean
index d809d8f87c..c5fa08032a 100644
--- a/tests/lean/run/coelambda.lean
+++ b/tests/lean/run/coelambda.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #eval #[2, 3, 1, 0].qsort fun a b => a < b
 #eval #[2, 3, 1, 0].qsort fun a b => let x := a; x < b
diff --git a/tests/lean/run/compiler_proj_bug.lean b/tests/lean/run/compiler_proj_bug.lean
index 31b030b513..3c63fac533 100644
--- a/tests/lean/run/compiler_proj_bug.lean
+++ b/tests/lean/run/compiler_proj_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure S :=
 (a : Nat) (h : a > 0) (b : Nat)
diff --git a/tests/lean/run/constantCompilerBug.lean b/tests/lean/run/constantCompilerBug.lean
index 1ab5b8f4e0..04d800930e 100644
--- a/tests/lean/run/constantCompilerBug.lean
+++ b/tests/lean/run/constantCompilerBug.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 open Lean
 open Lean.Parser
diff --git a/tests/lean/run/core.lean b/tests/lean/run/core.lean
index eb66c366f1..70002f8517 100644
--- a/tests/lean/run/core.lean
+++ b/tests/lean/run/core.lean
@@ -1,5 +1,5 @@
 import Lean.CoreM
-new_frontend
+
 open Lean
 open Lean.Core
 
diff --git a/tests/lean/run/csimp_type_error.lean b/tests/lean/run/csimp_type_error.lean
index 79d29ef7f5..357c6d1731 100644
--- a/tests/lean/run/csimp_type_error.lean
+++ b/tests/lean/run/csimp_type_error.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace scratch
 
diff --git a/tests/lean/run/def1.lean b/tests/lean/run/def1.lean
index 4d3f904df2..1eb4a18323 100644
--- a/tests/lean/run/def1.lean
+++ b/tests/lean/run/def1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive BV : Nat → Type
 | nil  : BV 0
diff --git a/tests/lean/run/def10.lean b/tests/lean/run/def10.lean
index 4cf71350c1..eb0de93d1c 100644
--- a/tests/lean/run/def10.lean
+++ b/tests/lean/run/def10.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f : Bool → Bool → Nat
 | _, _ => 10
diff --git a/tests/lean/run/def11.lean b/tests/lean/run/def11.lean
index 1b9edc43e5..ef5dd486b3 100644
--- a/tests/lean/run/def11.lean
+++ b/tests/lean/run/def11.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive Formula
 | eqf  : Nat → Nat → Formula
diff --git a/tests/lean/run/def12.lean b/tests/lean/run/def12.lean
index 43b1565e70..d3d731eea8 100644
--- a/tests/lean/run/def12.lean
+++ b/tests/lean/run/def12.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def diag : Bool → Bool → Bool → Nat
 | b,  true, false => 1
diff --git a/tests/lean/run/def13.lean b/tests/lean/run/def13.lean
index 9c2c14cf9e..933a734058 100644
--- a/tests/lean/run/def13.lean
+++ b/tests/lean/run/def13.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 variables {α} (p : α → Prop) [DecidablePred p]
 
diff --git a/tests/lean/run/def14.lean b/tests/lean/run/def14.lean
index a774be56ce..21866e3ad9 100644
--- a/tests/lean/run/def14.lean
+++ b/tests/lean/run/def14.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive Formula
 | eqf  : Nat → Nat → Formula
diff --git a/tests/lean/run/def15.lean b/tests/lean/run/def15.lean
index 6fb1a2f273..cbb00c9096 100644
--- a/tests/lean/run/def15.lean
+++ b/tests/lean/run/def15.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def head {α} : (as : List α) → as ≠ [] → α
 | [],    h => absurd rfl h
diff --git a/tests/lean/run/def16.lean b/tests/lean/run/def16.lean
index ff03909d56..cfc8e122e4 100644
--- a/tests/lean/run/def16.lean
+++ b/tests/lean/run/def16.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def half : Nat → Nat
 | 0     => 0
diff --git a/tests/lean/run/def17.lean b/tests/lean/run/def17.lean
index 4215323cb3..1c8cd36e74 100644
--- a/tests/lean/run/def17.lean
+++ b/tests/lean/run/def17.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def mk (a : Nat) : Nat → List Nat
 | 0   => []
diff --git a/tests/lean/run/def18.lean b/tests/lean/run/def18.lean
index 0581c4ad62..905782d148 100644
--- a/tests/lean/run/def18.lean
+++ b/tests/lean/run/def18.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universe u
 variable {α : Type u}
 
diff --git a/tests/lean/run/def19.lean b/tests/lean/run/def19.lean
index e0f8785041..e6724cb6ce 100644
--- a/tests/lean/run/def19.lean
+++ b/tests/lean/run/def19.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universe u
 
diff --git a/tests/lean/run/def2.lean b/tests/lean/run/def2.lean
index 088cf178b7..eeb03360d1 100644
--- a/tests/lean/run/def2.lean
+++ b/tests/lean/run/def2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive Vec.{u} (α : Type u) : Nat → Type u
 | nil  : Vec α 0
diff --git a/tests/lean/run/def20.lean b/tests/lean/run/def20.lean
index 2041cc77e3..3703500041 100644
--- a/tests/lean/run/def20.lean
+++ b/tests/lean/run/def20.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f : Char → Nat
 | 'a' => 0
diff --git a/tests/lean/run/def3.lean b/tests/lean/run/def3.lean
index ac41679e8e..dc669dbab5 100644
--- a/tests/lean/run/def3.lean
+++ b/tests/lean/run/def3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev N := Nat
 
diff --git a/tests/lean/run/def4.lean b/tests/lean/run/def4.lean
index 41f238bec5..a7f1bed40f 100644
--- a/tests/lean/run/def4.lean
+++ b/tests/lean/run/def4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive Foo : Bool → Type
 | Z  : Foo false
diff --git a/tests/lean/run/def5.lean b/tests/lean/run/def5.lean
index 8f333ff379..2ceb22b4ed 100644
--- a/tests/lean/run/def5.lean
+++ b/tests/lean/run/def5.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def fib : Nat → Nat
 | 0   => 1
diff --git a/tests/lean/run/def6.lean b/tests/lean/run/def6.lean
index dc7d9dd1a4..21737075aa 100644
--- a/tests/lean/run/def6.lean
+++ b/tests/lean/run/def6.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 open Nat
 
diff --git a/tests/lean/run/def7.lean b/tests/lean/run/def7.lean
index e460585a32..32a84a3e64 100644
--- a/tests/lean/run/def7.lean
+++ b/tests/lean/run/def7.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive InfTree.{u} (α : Type u)
 | leaf : α → InfTree α
diff --git a/tests/lean/run/def8.lean b/tests/lean/run/def8.lean
index 3fda48c1ff..5be2803e1e 100644
--- a/tests/lean/run/def8.lean
+++ b/tests/lean/run/def8.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def g : List Nat → List Nat → Nat
 | [],         y::ys => y
diff --git a/tests/lean/run/def9.lean b/tests/lean/run/def9.lean
index 751a4ebceb..7530fc74fc 100644
--- a/tests/lean/run/def9.lean
+++ b/tests/lean/run/def9.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f : Nat → Nat → Nat
 | 100, 2 => 0
diff --git a/tests/lean/run/depElim1.lean b/tests/lean/run/depElim1.lean
index aa1a1e1d92..572e043299 100644
--- a/tests/lean/run/depElim1.lean
+++ b/tests/lean/run/depElim1.lean
@@ -1,5 +1,5 @@
 import Lean.Meta.Match
-new_frontend
+
 open Lean
 open Lean.Meta
 open Lean.Meta.Match
diff --git a/tests/lean/run/deriv.lean b/tests/lean/run/deriv.lean
index 660c509765..223d68af88 100644
--- a/tests/lean/run/deriv.lean
+++ b/tests/lean/run/deriv.lean
@@ -1,6 +1,6 @@
 /- Benchmark for new code generator -/
 import Init.System.IO
-new_frontend
+
 
 inductive Expr
 | Val : Int → Expr
diff --git a/tests/lean/run/doNotation1.lean b/tests/lean/run/doNotation1.lean
index ddc8869dfb..4a7b89eb94 100644
--- a/tests/lean/run/doNotation1.lean
+++ b/tests/lean/run/doNotation1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 open Lean
 
 def f : IO Nat :=
diff --git a/tests/lean/run/doNotation2.lean b/tests/lean/run/doNotation2.lean
index a77fb1e8dc..1f3f7baf35 100644
--- a/tests/lean/run/doNotation2.lean
+++ b/tests/lean/run/doNotation2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : IO Nat := do
 IO.println "hello world"
diff --git a/tests/lean/run/doNotation3.lean b/tests/lean/run/doNotation3.lean
index 2a93b36d96..6bb70841e1 100644
--- a/tests/lean/run/doNotation3.lean
+++ b/tests/lean/run/doNotation3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem zeroLtOfLt : {a b : Nat} → a < b → 0 < b
 | 0,   _, h => h
diff --git a/tests/lean/run/doNotation4.lean b/tests/lean/run/doNotation4.lean
index 9d6e7a795a..4989b31ae7 100644
--- a/tests/lean/run/doNotation4.lean
+++ b/tests/lean/run/doNotation4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev M := StateRefT Nat IO
 
diff --git a/tests/lean/run/doNotation5.lean b/tests/lean/run/doNotation5.lean
index 3185c38436..9735b3fbe9 100644
--- a/tests/lean/run/doNotation5.lean
+++ b/tests/lean/run/doNotation5.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev M := ExceptT String $ ExceptT Nat $ StateM Nat
 
diff --git a/tests/lean/run/doNotation6.lean b/tests/lean/run/doNotation6.lean
index 60f8c701a6..ec750ba0c4 100644
--- a/tests/lean/run/doNotation6.lean
+++ b/tests/lean/run/doNotation6.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev M := StateRefT Nat IO
 
diff --git a/tests/lean/run/doTrailingAtEOI.lean b/tests/lean/run/doTrailingAtEOI.lean
index c0b174749b..e1a2178b95 100644
--- a/tests/lean/run/doTrailingAtEOI.lean
+++ b/tests/lean/run/doTrailingAtEOI.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 
 def f (x : Nat) : IO Nat := do
diff --git a/tests/lean/run/dofun_prec.lean b/tests/lean/run/dofun_prec.lean
index ffbdf4ad13..e5e37eecb5 100644
--- a/tests/lean/run/dofun_prec.lean
+++ b/tests/lean/run/dofun_prec.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst1 (x : Nat) : IO Unit := do
 if x > 0 then
diff --git a/tests/lean/run/dollarProjIssue.lean b/tests/lean/run/dollarProjIssue.lean
index a0654158d1..82001be6bf 100644
--- a/tests/lean/run/dollarProjIssue.lean
+++ b/tests/lean/run/dollarProjIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def g (x : Nat) : List (Nat × List Nat) :=
 [(x, [x, x]), (x, [])]
diff --git a/tests/lean/run/elabCmd.lean b/tests/lean/run/elabCmd.lean
index 06c4a7e093..1a7b17ae71 100644
--- a/tests/lean/run/elabCmd.lean
+++ b/tests/lean/run/elabCmd.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 open Lean
 open Lean.Elab
diff --git a/tests/lean/run/elabIte.lean b/tests/lean/run/elabIte.lean
index 88c619a3b5..8a0413f125 100644
--- a/tests/lean/run/elabIte.lean
+++ b/tests/lean/run/elabIte.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x y : Nat) : Option Nat :=
 if x > y then x else none
diff --git a/tests/lean/run/elab_cmd.lean b/tests/lean/run/elab_cmd.lean
index bc286b1337..67da01c8ef 100644
--- a/tests/lean/run/elab_cmd.lean
+++ b/tests/lean/run/elab_cmd.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 open Lean.Elab.Term
 open Lean.Elab.Command
diff --git a/tests/lean/run/etaFirst.lean b/tests/lean/run/etaFirst.lean
index 7742d34d12..9f055b63b4 100644
--- a/tests/lean/run/etaFirst.lean
+++ b/tests/lean/run/etaFirst.lean
@@ -2,7 +2,7 @@
 -- theorem tst1 : (fun a b => Nat.add a b) = Nat.add :=
 -- Eq.refl (fun a b => Nat.add a b)
 
-new_frontend
+
 
 theorem tst2 : (fun a b => Nat.add a b) = Nat.add :=
 Eq.refl (fun a b => Nat.add a b)
diff --git a/tests/lean/run/eval_unboxed_const.lean b/tests/lean/run/eval_unboxed_const.lean
index 17c64dd3bf..1246b8534e 100644
--- a/tests/lean/run/eval_unboxed_const.lean
+++ b/tests/lean/run/eval_unboxed_const.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 open Lean
 
diff --git a/tests/lean/run/evalconst.lean b/tests/lean/run/evalconst.lean
index 9cce6e24c5..43f1a962ae 100644
--- a/tests/lean/run/evalconst.lean
+++ b/tests/lean/run/evalconst.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 def x := 10
diff --git a/tests/lean/run/expectedTypePropagation.lean b/tests/lean/run/expectedTypePropagation.lean
index f20f5c8a96..1616b6be65 100644
--- a/tests/lean/run/expectedTypePropagation.lean
+++ b/tests/lean/run/expectedTypePropagation.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 instance : Coe Nat Int :=
 ⟨fun n => Int.ofNat n⟩
diff --git a/tests/lean/run/expr1.lean b/tests/lean/run/expr1.lean
index 01f1d9596c..1249b077f6 100644
--- a/tests/lean/run/expr1.lean
+++ b/tests/lean/run/expr1.lean
@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def tst1 : IO Unit :=
diff --git a/tests/lean/run/expr_maps.lean b/tests/lean/run/expr_maps.lean
index 27a86179e7..81d9dd90b2 100644
--- a/tests/lean/run/expr_maps.lean
+++ b/tests/lean/run/expr_maps.lean
@@ -1,5 +1,5 @@
 import Lean.Expr
-new_frontend
+
 open Lean
 
 def exprType : Expr := mkSort levelOne
diff --git a/tests/lean/run/extern.lean b/tests/lean/run/extern.lean
index 84a3c515d0..474a56e84d 100644
--- a/tests/lean/run/extern.lean
+++ b/tests/lean/run/extern.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 @[extern]
 def foo (x : Nat) := x
diff --git a/tests/lean/run/extmacro.lean b/tests/lean/run/extmacro.lean
index f8d9c5c21d..483bf56380 100644
--- a/tests/lean/run/extmacro.lean
+++ b/tests/lean/run/extmacro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro ext_tactic t:tactic "=>" newT:tactic : command => `(macro_rules | `($t) => `($newT))
 
diff --git a/tests/lean/run/finally.lean b/tests/lean/run/finally.lean
index 8ed09b8eaa..3a2e1e7850 100644
--- a/tests/lean/run/finally.lean
+++ b/tests/lean/run/finally.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def checkM (b : IO Bool) : IO Unit :=
 unlessM b (throw $ IO.userError "failed")
diff --git a/tests/lean/run/float1.lean b/tests/lean/run/float1.lean
index c2f315e8c8..ce3b041405 100644
--- a/tests/lean/run/float1.lean
+++ b/tests/lean/run/float1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def main : IO Unit := do
 IO.println ((2 : Float).sin);
diff --git a/tests/lean/run/float_cases_bug.lean b/tests/lean/run/float_cases_bug.lean
index b4b4df6eed..d35b00bb3d 100644
--- a/tests/lean/run/float_cases_bug.lean
+++ b/tests/lean/run/float_cases_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo (xs : List Nat) :=
 xs.span (fun n => (decide (n = 1)))
diff --git a/tests/lean/run/float_from_bignum.lean b/tests/lean/run/float_from_bignum.lean
index 8c6cb62390..d3587bad15 100644
--- a/tests/lean/run/float_from_bignum.lean
+++ b/tests/lean/run/float_from_bignum.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def check (b : Bool) : IO Unit :=
 «unless» b $ throw $ IO.userError "check failed"
diff --git a/tests/lean/run/floatarray.lean b/tests/lean/run/floatarray.lean
index 9a648a950a..9aa0a5d79c 100644
--- a/tests/lean/run/floatarray.lean
+++ b/tests/lean/run/floatarray.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst : IO Unit :=
 do
diff --git a/tests/lean/run/foldConsts.lean b/tests/lean/run/foldConsts.lean
index cbd0710f3a..52fcc1e880 100644
--- a/tests/lean/run/foldConsts.lean
+++ b/tests/lean/run/foldConsts.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 partial def mkTerm : Nat → Expr
diff --git a/tests/lean/run/forBodyResultTypeIssue.lean b/tests/lean/run/forBodyResultTypeIssue.lean
index de8e5ab973..9a9061d0e0 100644
--- a/tests/lean/run/forBodyResultTypeIssue.lean
+++ b/tests/lean/run/forBodyResultTypeIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev M := ExceptT String $ StateT Nat Id
 
diff --git a/tests/lean/run/fun.lean b/tests/lean/run/fun.lean
index dd3bb56eff..da0dca11da 100644
--- a/tests/lean/run/fun.lean
+++ b/tests/lean/run/fun.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 open Function Bool
 
diff --git a/tests/lean/run/generalize.lean b/tests/lean/run/generalize.lean
index 566463a8be..6765a5d24e 100644
--- a/tests/lean/run/generalize.lean
+++ b/tests/lean/run/generalize.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem tst0 (x : Nat) : x + 0 = x + 0 :=
 by {
diff --git a/tests/lean/run/generalizeTelescope.lean b/tests/lean/run/generalizeTelescope.lean
index 76d12f2698..ddb54ef572 100644
--- a/tests/lean/run/generalizeTelescope.lean
+++ b/tests/lean/run/generalizeTelescope.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/genindices.lean b/tests/lean/run/genindices.lean
index e9b42baaa0..b39c35f718 100644
--- a/tests/lean/run/genindices.lean
+++ b/tests/lean/run/genindices.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 universe u
 
 inductive Pred : ∀ (α : Type u), List α → Type (u+1)
diff --git a/tests/lean/run/getline_crash.lean b/tests/lean/run/getline_crash.lean
index 454899b995..a84b5db01b 100644
--- a/tests/lean/run/getline_crash.lean
+++ b/tests/lean/run/getline_crash.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tstGetLine (str : String) : IO Unit := do
 let path := "tmp_file";
diff --git a/tests/lean/run/impByNameResolution.lean b/tests/lean/run/impByNameResolution.lean
index b89909c1a8..15f3178767 100644
--- a/tests/lean/run/impByNameResolution.lean
+++ b/tests/lean/run/impByNameResolution.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 
diff --git a/tests/lean/run/implicitTypesRecCoe.lean b/tests/lean/run/implicitTypesRecCoe.lean
index ed330fd532..b24ad0cce6 100644
--- a/tests/lean/run/implicitTypesRecCoe.lean
+++ b/tests/lean/run/implicitTypesRecCoe.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 unsafe def f (n : Nat) :=
 let rec g (x : Nat) :=
diff --git a/tests/lean/run/incmd.lean b/tests/lean/run/incmd.lean
index 508d430fe9..7333fcbfd6 100644
--- a/tests/lean/run/incmd.lean
+++ b/tests/lean/run/incmd.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 variable {α : Type} in
 def f : α → α :=
diff --git a/tests/lean/run/ind_cmd_bug.lean b/tests/lean/run/ind_cmd_bug.lean
index ddaf7f5792..5115b00415 100644
--- a/tests/lean/run/ind_cmd_bug.lean
+++ b/tests/lean/run/ind_cmd_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure D (α : Type) :=
 (a : α)
diff --git a/tests/lean/run/induction1.lean b/tests/lean/run/induction1.lean
index d5d2c458ca..71e86fbebe 100644
--- a/tests/lean/run/induction1.lean
+++ b/tests/lean/run/induction1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 @[recursor 4]
 def Or.elim2 {p q r : Prop} (major : p ∨ q) (left : p → r) (right : q → r) : r :=
diff --git a/tests/lean/run/inductive1.lean b/tests/lean/run/inductive1.lean
index f8f4785e24..64615db759 100644
--- a/tests/lean/run/inductive1.lean
+++ b/tests/lean/run/inductive1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive L1.{u} (α : Type u)
 | nil
diff --git a/tests/lean/run/inductive2.lean b/tests/lean/run/inductive2.lean
index cf44465120..e4d7563ec0 100644
--- a/tests/lean/run/inductive2.lean
+++ b/tests/lean/run/inductive2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 mutual
 universe u
diff --git a/tests/lean/run/inj1.lean b/tests/lean/run/inj1.lean
index 71505264f1..91ebec82a9 100644
--- a/tests/lean/run/inj1.lean
+++ b/tests/lean/run/inj1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem test1 {α} (a b : α) (as bs : List α) (h : a::as = b::bs) : a = b :=
 by {
diff --git a/tests/lean/run/inj2.lean b/tests/lean/run/inj2.lean
index c3cb498e3e..a195a0b2f0 100644
--- a/tests/lean/run/inj2.lean
+++ b/tests/lean/run/inj2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v
 
diff --git a/tests/lean/run/inline_fn.lean b/tests/lean/run/inline_fn.lean
index dcc48049f1..c0908a1d29 100644
--- a/tests/lean/run/inline_fn.lean
+++ b/tests/lean/run/inline_fn.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f {α : Type} [HasAdd α] (x : α) :=
 x + x + x
diff --git a/tests/lean/run/inliner_loop.lean b/tests/lean/run/inliner_loop.lean
index 30e8e27219..d95128c84c 100644
--- a/tests/lean/run/inliner_loop.lean
+++ b/tests/lean/run/inliner_loop.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 unsafe inductive t
 | mk : (t → t) → t
diff --git a/tests/lean/run/instances.lean b/tests/lean/run/instances.lean
index b2e34d44ff..0c95b63c05 100644
--- a/tests/lean/run/instances.lean
+++ b/tests/lean/run/instances.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/instuniv.lean b/tests/lean/run/instuniv.lean
index a194f2c3ad..be578dc5b6 100644
--- a/tests/lean/run/instuniv.lean
+++ b/tests/lean/run/instuniv.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 unsafe def tst : IO Unit :=
diff --git a/tests/lean/run/int_to_nat_bug.lean b/tests/lean/run/int_to_nat_bug.lean
index f0088f095d..10dee98365 100644
--- a/tests/lean/run/int_to_nat_bug.lean
+++ b/tests/lean/run/int_to_nat_bug.lean
@@ -1,2 +1,2 @@
-new_frontend
+
 #eval (4294967295 : Int)
diff --git a/tests/lean/run/intromacro.lean b/tests/lean/run/intromacro.lean
index d62157ee14..f7e5ccf1fe 100644
--- a/tests/lean/run/intromacro.lean
+++ b/tests/lean/run/intromacro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure S :=
 (x y z : Nat := 0)
diff --git a/tests/lean/run/irCompilerBug.lean b/tests/lean/run/irCompilerBug.lean
index 50f3543264..00afd8fd15 100644
--- a/tests/lean/run/irCompilerBug.lean
+++ b/tests/lean/run/irCompilerBug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure Payload :=
 (key : Nat)
diff --git a/tests/lean/run/kernel1.lean b/tests/lean/run/kernel1.lean
index a5d8f12bdc..eb20feca73 100644
--- a/tests/lean/run/kernel1.lean
+++ b/tests/lean/run/kernel1.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 def checkDefEq (a b : Name) : CoreM Unit := do
diff --git a/tests/lean/run/kernel2.lean b/tests/lean/run/kernel2.lean
index f493d79c87..367c2f2807 100644
--- a/tests/lean/run/kernel2.lean
+++ b/tests/lean/run/kernel2.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 def checkDefEq (a b : Name) : CoreM Unit := do
diff --git a/tests/lean/run/kevin.lean b/tests/lean/run/kevin.lean
index ebe86b1fdb..406000b802 100644
--- a/tests/lean/run/kevin.lean
+++ b/tests/lean/run/kevin.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 macro:10000 x:term "ⁿ" : term => `($x ^ $(mkIdent `n))
diff --git a/tests/lean/run/level.lean b/tests/lean/run/level.lean
index 553253258c..241a5ac270 100644
--- a/tests/lean/run/level.lean
+++ b/tests/lean/run/level.lean
@@ -1,5 +1,5 @@
 import Lean.Level
-new_frontend
+
 open Lean
 
 #eval levelZero == levelZero
diff --git a/tests/lean/run/localNameResolutionWithProj.lean b/tests/lean/run/localNameResolutionWithProj.lean
index 4016d21a2f..d15d59d7fb 100644
--- a/tests/lean/run/localNameResolutionWithProj.lean
+++ b/tests/lean/run/localNameResolutionWithProj.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro "foo!" x:term : term => `(let xs := $x; xs.succ + xs)
 
diff --git a/tests/lean/run/macro.lean b/tests/lean/run/macro.lean
index 1cf032f830..c4b69e4da6 100644
--- a/tests/lean/run/macro.lean
+++ b/tests/lean/run/macro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev Set (α : Type) := α → Prop
 axiom setOf {α : Type} : (α → Prop) → Set α
diff --git a/tests/lean/run/macro2.lean b/tests/lean/run/macro2.lean
index f784d72cb3..1e3bcc48b8 100644
--- a/tests/lean/run/macro2.lean
+++ b/tests/lean/run/macro2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 notation:50 a `**` b:50 => b * a * b
 notation "~" a => a+a
diff --git a/tests/lean/run/macro3.lean b/tests/lean/run/macro3.lean
index a01370fa13..2e354328a5 100644
--- a/tests/lean/run/macro3.lean
+++ b/tests/lean/run/macro3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax "call" term:max "(" (sepBy1 term ",") ")" : term
 
diff --git a/tests/lean/run/macro_macro.lean b/tests/lean/run/macro_macro.lean
index df866d79a8..6ff125bc51 100644
--- a/tests/lean/run/macro_macro.lean
+++ b/tests/lean/run/macro_macro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro mk_m id:ident v:str n:num c:char : command => `(macro $id:ident : term => `(fun (x : String) => x ++ $v ++ toString $n ++ toString $c))
 
diff --git a/tests/lean/run/macroid.lean b/tests/lean/run/macroid.lean
index 6c73010350..20735a4dc6 100644
--- a/tests/lean/run/macroid.lean
+++ b/tests/lean/run/macroid.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax "[" ident "↦" term "]" : term
 macro_rules `([$x ↦ $v]) => `(fun $x => $v)
diff --git a/tests/lean/run/match1.lean b/tests/lean/run/match1.lean
index d7967bf109..21c9a976dd 100644
--- a/tests/lean/run/match1.lean
+++ b/tests/lean/run/match1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (xs : List Nat) : List Bool :=
 xs.map fun
diff --git a/tests/lean/run/matchArrayLit.lean b/tests/lean/run/matchArrayLit.lean
index c25fb8f024..39559462d1 100644
--- a/tests/lean/run/matchArrayLit.lean
+++ b/tests/lean/run/matchArrayLit.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u v
 
 theorem eqLitOfSize0 {α : Type u} (a : Array α) (hsz : a.size = 0) : a = #[] :=
diff --git a/tests/lean/run/matchDiscrType.lean b/tests/lean/run/matchDiscrType.lean
index c29a281c64..f3db24705b 100644
--- a/tests/lean/run/matchDiscrType.lean
+++ b/tests/lean/run/matchDiscrType.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def g (x : Nat) : List (Nat × List Nat) :=
 [(x, [x, x]), (x, [])]
diff --git a/tests/lean/run/matcherElimUniv.lean b/tests/lean/run/matcherElimUniv.lean
index c412ecea00..5bcfeef68b 100644
--- a/tests/lean/run/matcherElimUniv.lean
+++ b/tests/lean/run/matcherElimUniv.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u
 
 def len {α : Type u} : List α → List α → Nat
diff --git a/tests/lean/run/matchtac.lean b/tests/lean/run/matchtac.lean
index 3df10bf5f5..e1149f242d 100644
--- a/tests/lean/run/matchtac.lean
+++ b/tests/lean/run/matchtac.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem tst1 {α : Type} {p : Prop} (xs : List α) (h₁ : (a : α) → (as : List α) → xs = a :: as → p) (h₂ : xs = [] → p) : p :=
 by match h:xs with
diff --git a/tests/lean/run/meta1.lean b/tests/lean/run/meta1.lean
index 8752777f1a..16f44d9815 100644
--- a/tests/lean/run/meta1.lean
+++ b/tests/lean/run/meta1.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta3.lean b/tests/lean/run/meta3.lean
index ddce3afc32..c571b7554a 100644
--- a/tests/lean/run/meta3.lean
+++ b/tests/lean/run/meta3.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta4.lean b/tests/lean/run/meta4.lean
index dd5322d1ee..9073e77f48 100644
--- a/tests/lean/run/meta4.lean
+++ b/tests/lean/run/meta4.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta5.lean b/tests/lean/run/meta5.lean
index 62e93d3f8c..0664ae994d 100644
--- a/tests/lean/run/meta5.lean
+++ b/tests/lean/run/meta5.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta6.lean b/tests/lean/run/meta6.lean
index bf3ddd841a..8ba7fb1951 100644
--- a/tests/lean/run/meta6.lean
+++ b/tests/lean/run/meta6.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/meta7.lean b/tests/lean/run/meta7.lean
index 4ffd6c4e24..d619a81801 100644
--- a/tests/lean/run/meta7.lean
+++ b/tests/lean/run/meta7.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/mixedMacroRules.lean b/tests/lean/run/mixedMacroRules.lean
index c158eaaeb2..8bfa03eb0a 100644
--- a/tests/lean/run/mixedMacroRules.lean
+++ b/tests/lean/run/mixedMacroRules.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 syntax:65 term "+!+" term:65 : term
 syntax:70 term "*!*" term:70 : term
diff --git a/tests/lean/run/mixfix.lean b/tests/lean/run/mixfix.lean
index b2ec9fb46f..b1f15dae48 100644
--- a/tests/lean/run/mixfix.lean
+++ b/tests/lean/run/mixfix.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 infix:65 " +' " => HasAdd.add
 infix:70 " *' " => HasMul.mul
diff --git a/tests/lean/run/monadCache.lean b/tests/lean/run/monadCache.lean
index 4d0c071fb8..bf8e3737b0 100644
--- a/tests/lean/run/monadCache.lean
+++ b/tests/lean/run/monadCache.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 partial def mkTower : Nat → Expr
diff --git a/tests/lean/run/monadControl.lean b/tests/lean/run/monadControl.lean
index 2b1971b464..d007ab27d0 100644
--- a/tests/lean/run/monadControl.lean
+++ b/tests/lean/run/monadControl.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 @[inline] def f {α} (s : String) (x : IO α) : IO α := do
 IO.println "started";
diff --git a/tests/lean/run/namespaceIssue.lean b/tests/lean/run/namespaceIssue.lean
index be7d67d78b..987e13d9ae 100644
--- a/tests/lean/run/namespaceIssue.lean
+++ b/tests/lean/run/namespaceIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def Bla.x := 10
 
diff --git a/tests/lean/run/nativeReflBackdoor.lean b/tests/lean/run/nativeReflBackdoor.lean
index 89e011a03f..fadd241dac 100644
--- a/tests/lean/run/nativeReflBackdoor.lean
+++ b/tests/lean/run/nativeReflBackdoor.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 /-
 This example demonstratea that when we are using `nativeRefl!`,
diff --git a/tests/lean/run/natlit.lean b/tests/lean/run/natlit.lean
index 8c0f61426e..c3b5654da3 100644
--- a/tests/lean/run/natlit.lean
+++ b/tests/lean/run/natlit.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst1 : 0 + 1 = 1 := rfl
 def tst2 : 2 + 3 = 5 := rfl
diff --git a/tests/lean/run/nested_match_bug.lean b/tests/lean/run/nested_match_bug.lean
index 119c6e34fa..7f37810f5b 100644
--- a/tests/lean/run/nested_match_bug.lean
+++ b/tests/lean/run/nested_match_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 inductive Term : Type
 | app : List Term -> Term
diff --git a/tests/lean/run/new_compiler.lean b/tests/lean/run/new_compiler.lean
index 2db78aeec4..0fa118a081 100644
--- a/tests/lean/run/new_compiler.lean
+++ b/tests/lean/run/new_compiler.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v w r s
 
diff --git a/tests/lean/run/new_frontend2.lean b/tests/lean/run/new_frontend2.lean
index b913ad8f55..42479407f1 100644
--- a/tests/lean/run/new_frontend2.lean
+++ b/tests/lean/run/new_frontend2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 declare_syntax_cat foo
 
diff --git a/tests/lean/run/new_inductive.lean b/tests/lean/run/new_inductive.lean
index e9a31f3474..25eacb6f0b 100644
--- a/tests/lean/run/new_inductive.lean
+++ b/tests/lean/run/new_inductive.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u v
 
 inductive myList (α : Type u)
diff --git a/tests/lean/run/new_inductive2.lean b/tests/lean/run/new_inductive2.lean
index e08dec06cb..fd92c6be7c 100644
--- a/tests/lean/run/new_inductive2.lean
+++ b/tests/lean/run/new_inductive2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v
 
diff --git a/tests/lean/run/newfrontend1.lean b/tests/lean/run/newfrontend1.lean
index 9e458a25fa..edd4ce858f 100644
--- a/tests/lean/run/newfrontend1.lean
+++ b/tests/lean/run/newfrontend1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def x := 1
 
 #check x
diff --git a/tests/lean/run/newfrontend2.lean b/tests/lean/run/newfrontend2.lean
index 8ded42cfd4..4f9f2c4347 100644
--- a/tests/lean/run/newfrontend2.lean
+++ b/tests/lean/run/newfrontend2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo {α} (a : Option α) (b : α) : α  :=
 match a with
diff --git a/tests/lean/run/newfrontend3.lean b/tests/lean/run/newfrontend3.lean
index a37b013e91..c6f488fbd6 100644
--- a/tests/lean/run/newfrontend3.lean
+++ b/tests/lean/run/newfrontend3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure S  :=
 (g {α} : α → α)
diff --git a/tests/lean/run/newfrontend5.lean b/tests/lean/run/newfrontend5.lean
index 636124a464..61f60d6977 100644
--- a/tests/lean/run/newfrontend5.lean
+++ b/tests/lean/run/newfrontend5.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def foo {α} (f : {β : Type _} → β → β) (a : α) : α :=
 f a
diff --git a/tests/lean/run/nicerNestedDos.lean b/tests/lean/run/nicerNestedDos.lean
index 2a3dae023e..bf7df4d76f 100644
--- a/tests/lean/run/nicerNestedDos.lean
+++ b/tests/lean/run/nicerNestedDos.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) : IO Nat := do
 IO.println "hello"
diff --git a/tests/lean/run/noncomputable_bug.lean b/tests/lean/run/noncomputable_bug.lean
index f09f5032ba..2441cd44b9 100644
--- a/tests/lean/run/noncomputable_bug.lean
+++ b/tests/lean/run/noncomputable_bug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 axiom f : ∀ (A : Type), A → Type
 
diff --git a/tests/lean/run/obtain.lean b/tests/lean/run/obtain.lean
index 4f5565439d..875169f969 100644
--- a/tests/lean/run/obtain.lean
+++ b/tests/lean/run/obtain.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro "obtain " p:term " from " d:term "; " body:term : term =>
 `(match $d:term with | $p:term => $body:term)
diff --git a/tests/lean/run/optParam.lean b/tests/lean/run/optParam.lean
index fe7b4e65e1..fdb3cc224a 100644
--- a/tests/lean/run/optParam.lean
+++ b/tests/lean/run/optParam.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def p (x : Nat := 0) : Nat × Nat :=
 (x, x)
diff --git a/tests/lean/run/overloaded.lean b/tests/lean/run/overloaded.lean
index 1929fe664b..cee631d57b 100644
--- a/tests/lean/run/overloaded.lean
+++ b/tests/lean/run/overloaded.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def A.x : Nat := 10
 def B.x : String := "hello"
diff --git a/tests/lean/run/partial1.lean b/tests/lean/run/partial1.lean
index f79ae396ed..863bd30ab7 100644
--- a/tests/lean/run/partial1.lean
+++ b/tests/lean/run/partial1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 partial def reverse {α} (as : List α) : List α :=
 let rec loop : List α → List α → List α
diff --git a/tests/lean/run/partialApp.lean b/tests/lean/run/partialApp.lean
index 7b78abb734..ba3a699698 100644
--- a/tests/lean/run/partialApp.lean
+++ b/tests/lean/run/partialApp.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (x : Nat) (y : Nat := 1) (w : Nat := 2) (z : Nat) :=
 x + y + w - z
diff --git a/tests/lean/run/patbug.lean b/tests/lean/run/patbug.lean
index d5e07c85dc..93cdfadecd 100644
--- a/tests/lean/run/patbug.lean
+++ b/tests/lean/run/patbug.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 open Lean
 
 def f : Name → Name
diff --git a/tests/lean/run/print_cmd.lean b/tests/lean/run/print_cmd.lean
index 53e2a49792..860f16d5fd 100644
--- a/tests/lean/run/print_cmd.lean
+++ b/tests/lean/run/print_cmd.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 #print Nat
 
 private def foo (x : Nat) : Nat := x + 1
diff --git a/tests/lean/run/proofIrrelFVar.lean b/tests/lean/run/proofIrrelFVar.lean
index 899e2501b0..a91a28bcbf 100644
--- a/tests/lean/run/proofIrrelFVar.lean
+++ b/tests/lean/run/proofIrrelFVar.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u
 variables {α : Type u} {p : α → Prop}
 
diff --git a/tests/lean/run/prv.lean b/tests/lean/run/prv.lean
index 3e0a37c05b..d56bb67311 100644
--- a/tests/lean/run/prv.lean
+++ b/tests/lean/run/prv.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 private def x := 10
 
diff --git a/tests/lean/run/ptrAddr.lean b/tests/lean/run/ptrAddr.lean
index dabac248d4..0b96324479 100644
--- a/tests/lean/run/ptrAddr.lean
+++ b/tests/lean/run/ptrAddr.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 axiom TrustMe {p : Prop} : p
 
diff --git a/tests/lean/run/quasi_pattern_unification_approx_issue.lean b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
index 87c1ed19d9..33aa4dde64 100644
--- a/tests/lean/run/quasi_pattern_unification_approx_issue.lean
+++ b/tests/lean/run/quasi_pattern_unification_approx_issue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 variables {δ σ : Type}
 
diff --git a/tests/lean/run/range.lean b/tests/lean/run/range.lean
index 2538f32dbe..3d499ab209 100644
--- a/tests/lean/run/range.lean
+++ b/tests/lean/run/range.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def ex1 : IO Unit := do
 IO.println "example 1"
diff --git a/tests/lean/run/rc_tests.lean b/tests/lean/run/rc_tests.lean
index bae15d52c4..3c30d96767 100644
--- a/tests/lean/run/rc_tests.lean
+++ b/tests/lean/run/rc_tests.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u v
 
 -- setOption pp.binderTypes False
diff --git a/tests/lean/run/readerThe.lean b/tests/lean/run/readerThe.lean
index 469f6e0e02..c091159709 100644
--- a/tests/lean/run/readerThe.lean
+++ b/tests/lean/run/readerThe.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 abbrev M := ReaderT String $ StateT Nat $ ReaderT Bool $ IO
 
diff --git a/tests/lean/run/recInfo1.lean b/tests/lean/run/recInfo1.lean
index 58758c0c68..8f7f148f7e 100644
--- a/tests/lean/run/recInfo1.lean
+++ b/tests/lean/run/recInfo1.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/reduce1.lean b/tests/lean/run/reduce1.lean
index 838971e232..8a91cd69be 100644
--- a/tests/lean/run/reduce1.lean
+++ b/tests/lean/run/reduce1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 partial def fact : Nat → Nat
 | 0     => 1
diff --git a/tests/lean/run/replace.lean b/tests/lean/run/replace.lean
index ff3e82e29b..eedc78c1d6 100644
--- a/tests/lean/run/replace.lean
+++ b/tests/lean/run/replace.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 partial def mkBig : Nat → Expr
diff --git a/tests/lean/run/resolveLVal.lean b/tests/lean/run/resolveLVal.lean
index 548aa3935e..78f89c2763 100644
--- a/tests/lean/run/resolveLVal.lean
+++ b/tests/lean/run/resolveLVal.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 
diff --git a/tests/lean/run/revert1.lean b/tests/lean/run/revert1.lean
index 620b77bbf9..707573a183 100644
--- a/tests/lean/run/revert1.lean
+++ b/tests/lean/run/revert1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem tst1 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
diff --git a/tests/lean/run/scc.lean b/tests/lean/run/scc.lean
index bd10ea3eda..a7c323a8ea 100644
--- a/tests/lean/run/scc.lean
+++ b/tests/lean/run/scc.lean
@@ -1,5 +1,5 @@
 import Lean.Util.SCC
-new_frontend
+
 open Lean.SCC
 
 def checkSCC (expected : List (List Nat)) (vertices : List Nat) (successorsOf : Nat → List Nat) : IO Unit := do
diff --git a/tests/lean/run/sharecommon.lean b/tests/lean/run/sharecommon.lean
index 8111360da7..5d93d5b3e9 100644
--- a/tests/lean/run/sharecommon.lean
+++ b/tests/lean/run/sharecommon.lean
@@ -1,5 +1,5 @@
 import Std.ShareCommon
-new_frontend
+
 open Std
 def check (b : Bool) : ShareCommonT IO Unit := do
 unless b do throw $ IO.userError "check failed"
diff --git a/tests/lean/run/spec_issue.lean b/tests/lean/run/spec_issue.lean
index 94e4edb10b..a083563ea2 100644
--- a/tests/lean/run/spec_issue.lean
+++ b/tests/lean/run/spec_issue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 set_option trace.compiler.ir.result true
 
 def g (ys : List Nat) : IO Nat := do
diff --git a/tests/lean/run/stateRef.lean b/tests/lean/run/stateRef.lean
index 9438d59ad9..1893c34850 100644
--- a/tests/lean/run/stateRef.lean
+++ b/tests/lean/run/stateRef.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (v : Nat) : StateRefT Nat IO Nat := do
 IO.println "hello"
diff --git a/tests/lean/run/strInterpolation.lean b/tests/lean/run/strInterpolation.lean
index 5d348ab557..5f51880ea4 100644
--- a/tests/lean/run/strInterpolation.lean
+++ b/tests/lean/run/strInterpolation.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #eval s!"hello {1+1}"
 
diff --git a/tests/lean/run/struct1.lean b/tests/lean/run/struct1.lean
index 6273d5c921..a83f4578cf 100644
--- a/tests/lean/run/struct1.lean
+++ b/tests/lean/run/struct1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure A0.{u} (α : Type u) :=
 (x : α)
diff --git a/tests/lean/run/struct2.lean b/tests/lean/run/struct2.lean
index f5dba10674..8d4b1b0817 100644
--- a/tests/lean/run/struct2.lean
+++ b/tests/lean/run/struct2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universe u
 
diff --git a/tests/lean/run/struct3.lean b/tests/lean/run/struct3.lean
index 073ecdda9c..9df477fd63 100644
--- a/tests/lean/run/struct3.lean
+++ b/tests/lean/run/struct3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 universes u v
 
diff --git a/tests/lean/run/structInst.lean b/tests/lean/run/structInst.lean
index 0dfa3d4e46..8d1ec21983 100644
--- a/tests/lean/run/structInst.lean
+++ b/tests/lean/run/structInst.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Ex1
 
diff --git a/tests/lean/run/structInst2.lean b/tests/lean/run/structInst2.lean
index 85f009b56e..6f5fda2a36 100644
--- a/tests/lean/run/structInst2.lean
+++ b/tests/lean/run/structInst2.lean
@@ -1,5 +1,5 @@
 import Init.Control.Option
-new_frontend
+
 
 universes u v
 
diff --git a/tests/lean/run/structInst3.lean b/tests/lean/run/structInst3.lean
index 4b73a8c7b7..c43fee2816 100644
--- a/tests/lean/run/structInst3.lean
+++ b/tests/lean/run/structInst3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u
 
 namespace Ex1
diff --git a/tests/lean/run/structInst4.lean b/tests/lean/run/structInst4.lean
index 8e84609a7c..6fa6066fbb 100644
--- a/tests/lean/run/structInst4.lean
+++ b/tests/lean/run/structInst4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 universes u
 
 def a : Array ((Nat × Nat) × Bool) := #[]
diff --git a/tests/lean/run/struct_inst_typed.lean b/tests/lean/run/struct_inst_typed.lean
index 646beb5126..02de514f66 100644
--- a/tests/lean/run/struct_inst_typed.lean
+++ b/tests/lean/run/struct_inst_typed.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 #check { fst := 10, snd := 20 : Nat × Nat }
 
 structure S :=
diff --git a/tests/lean/run/struct_instance_in_eqn.lean b/tests/lean/run/struct_instance_in_eqn.lean
index 44e64f92dd..f1090569b1 100644
--- a/tests/lean/run/struct_instance_in_eqn.lean
+++ b/tests/lean/run/struct_instance_in_eqn.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure S :=
 (x : Nat) (y : Bool) (z : Nat) (w : Nat)
diff --git a/tests/lean/run/structuralIssue.lean b/tests/lean/run/structuralIssue.lean
index 45588e3fe6..5f37f1360e 100644
--- a/tests/lean/run/structuralIssue.lean
+++ b/tests/lean/run/structuralIssue.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f (xs : List Nat) : Nat :=
 match xs with
diff --git a/tests/lean/run/structuralRec1.lean b/tests/lean/run/structuralRec1.lean
index 743536237d..edec25e034 100644
--- a/tests/lean/run/structuralRec1.lean
+++ b/tests/lean/run/structuralRec1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def map {α β} (f : α → β) : List α → List β
 | []    => []
diff --git a/tests/lean/run/structure.lean b/tests/lean/run/structure.lean
index 68c2afd6d3..e674284fd2 100644
--- a/tests/lean/run/structure.lean
+++ b/tests/lean/run/structure.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 structure S1 :=
diff --git a/tests/lean/run/stxKindInsideNamespace.lean b/tests/lean/run/stxKindInsideNamespace.lean
index 9103957e6d..e8bc2ba8e9 100644
--- a/tests/lean/run/stxKindInsideNamespace.lean
+++ b/tests/lean/run/stxKindInsideNamespace.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace Foo
 
diff --git a/tests/lean/run/stxMacro.lean b/tests/lean/run/stxMacro.lean
index d90e486cde..32522daa6a 100644
--- a/tests/lean/run/stxMacro.lean
+++ b/tests/lean/run/stxMacro.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 -- Macro for the `syntax` category
 macro "many " x:stx : stx => `(stx| ($x)*)
diff --git a/tests/lean/run/subst1.lean b/tests/lean/run/subst1.lean
index 8aedd50c37..393f2d8dcd 100644
--- a/tests/lean/run/subst1.lean
+++ b/tests/lean/run/subst1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 set_option trace.Meta.Tactic.subst true
 
diff --git a/tests/lean/run/synth1.lean b/tests/lean/run/synth1.lean
index d81ef8ce19..101d5fce4a 100644
--- a/tests/lean/run/synth1.lean
+++ b/tests/lean/run/synth1.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 open Lean
 open Lean.Meta
 
diff --git a/tests/lean/run/synthPending1.lean b/tests/lean/run/synthPending1.lean
index d0acc0580c..d7231a21c0 100644
--- a/tests/lean/run/synthPending1.lean
+++ b/tests/lean/run/synthPending1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem ex : Not (1 = 2) :=
 ofDecideEqFalse rfl
diff --git a/tests/lean/run/tactic.lean b/tests/lean/run/tactic.lean
index e5ba93f9e3..9611104544 100644
--- a/tests/lean/run/tactic.lean
+++ b/tests/lean/run/tactic.lean
@@ -1,5 +1,5 @@
 import Lean.Meta
-new_frontend
+
 
 open Lean
 open Lean.Meta
diff --git a/tests/lean/run/tactic1.lean b/tests/lean/run/tactic1.lean
index 88717dcab4..76df973beb 100644
--- a/tests/lean/run/tactic1.lean
+++ b/tests/lean/run/tactic1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 theorem ex1 (x : Nat) (y : { v // v > x }) (z : Nat) : Nat :=
 by {
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index 60c1ab4eb8..3c5f341a01 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 open Lean
 
diff --git a/tests/lean/run/task_test.lean b/tests/lean/run/task_test.lean
index 155a4e958c..f51897ce53 100644
--- a/tests/lean/run/task_test.lean
+++ b/tests/lean/run/task_test.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def g (x : Nat) : Nat :=
 dbgTrace ("g: " ++ toString x) $ fun _ =>
diff --git a/tests/lean/run/task_test2.lean b/tests/lean/run/task_test2.lean
index 6f804763f1..61ea3c2122 100644
--- a/tests/lean/run/task_test2.lean
+++ b/tests/lean/run/task_test2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def run1 (i : Nat) (n : Nat) (xs : List Nat) : Nat :=
 n.repeat (fun r =>
diff --git a/tests/lean/run/termElab.lean b/tests/lean/run/termElab.lean
index 885635588e..6e2fad2a99 100644
--- a/tests/lean/run/termElab.lean
+++ b/tests/lean/run/termElab.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 open Lean
 open Lean.Elab
diff --git a/tests/lean/run/termParserAttr.lean b/tests/lean/run/termParserAttr.lean
index db8c7234fa..0a6ea1d13b 100644
--- a/tests/lean/run/termParserAttr.lean
+++ b/tests/lean/run/termParserAttr.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 open Lean.Elab
 
diff --git a/tests/lean/run/termparsertest1.lean b/tests/lean/run/termparsertest1.lean
index a36f803753..02c7f747c4 100644
--- a/tests/lean/run/termparsertest1.lean
+++ b/tests/lean/run/termparsertest1.lean
@@ -1,5 +1,5 @@
 import Lean.Parser.Term
-new_frontend
+
 open Lean
 open Lean.Parser
 
diff --git a/tests/lean/run/toExpr.lean b/tests/lean/run/toExpr.lean
index 1822a5911a..4ce97e7b24 100644
--- a/tests/lean/run/toExpr.lean
+++ b/tests/lean/run/toExpr.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 unsafe def test {α : Type} [HasToString α] [ToExpr α] [HasBeq α] (a : α) : CoreM Unit := do
diff --git a/tests/lean/run/trace.lean b/tests/lean/run/trace.lean
index e3e4c1c40f..ff569475b5 100644
--- a/tests/lean/run/trace.lean
+++ b/tests/lean/run/trace.lean
@@ -1,5 +1,5 @@
 import Lean.CoreM
-new_frontend
+
 open Lean
 
 structure MyState :=
diff --git a/tests/lean/run/tryPureCoe.lean b/tests/lean/run/tryPureCoe.lean
index 98c6e895f8..effb0c858e 100644
--- a/tests/lean/run/tryPureCoe.lean
+++ b/tests/lean/run/tryPureCoe.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def m1 : IO Bool :=
 pure true
 
diff --git a/tests/lean/run/type_class_performance1.lean b/tests/lean/run/type_class_performance1.lean
index 8de8faeba0..e10a2fd930 100644
--- a/tests/lean/run/type_class_performance1.lean
+++ b/tests/lean/run/type_class_performance1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #print USize
 
diff --git a/tests/lean/run/typeclass_append.lean b/tests/lean/run/typeclass_append.lean
index 85635638a0..76c6e7543b 100644
--- a/tests/lean/run/typeclass_append.lean
+++ b/tests/lean/run/typeclass_append.lean
@@ -5,7 +5,7 @@ Authors: Daniel Selsam
 
 Performance test to ensure quadratic blowup is avoided.
 -/
-new_frontend
+
 
 class Append {α : Type} (xs₁ xs₂ : List α) (out : outParam $ List α) : Type :=
 (u : Unit := ())
diff --git a/tests/lean/run/typeclass_coerce.lean b/tests/lean/run/typeclass_coerce.lean
index adfe916d97..8346199f0d 100644
--- a/tests/lean/run/typeclass_coerce.lean
+++ b/tests/lean/run/typeclass_coerce.lean
@@ -6,7 +6,7 @@ Authors: Daniel Selsam, Leonardo de Moura
 Declare new, simpler coercion class without the special support for transitivity.
 Test that new tabled typeclass resolution deals with loops and diamonds correctly.
 -/
-new_frontend
+
 
 class HasCoerce (a b : Type) :=
 (coerce : a → b)
diff --git a/tests/lean/run/typeclass_diamond.lean b/tests/lean/run/typeclass_diamond.lean
index a48898e862..519c30f983 100644
--- a/tests/lean/run/typeclass_diamond.lean
+++ b/tests/lean/run/typeclass_diamond.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 class Top₁   (n : Nat) : Type := (u : Unit := ())
 class Bot₁   (n : Nat) : Type := (u : Unit := ())
 class Left₁  (n : Nat) : Type := (u : Unit := ())
diff --git a/tests/lean/run/typeclass_easy.lean b/tests/lean/run/typeclass_easy.lean
index da3b441542..5758d404e4 100644
--- a/tests/lean/run/typeclass_easy.lean
+++ b/tests/lean/run/typeclass_easy.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 #synth HasToString (Nat × (Nat × Bool))
 
diff --git a/tests/lean/run/typeclass_loop.lean b/tests/lean/run/typeclass_loop.lean
index 64faf2edcd..d872a7e269 100644
--- a/tests/lean/run/typeclass_loop.lean
+++ b/tests/lean/run/typeclass_loop.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 example (M : Type → Type) [Monad M] : ExceptT Unit (ReaderT Unit (StateT Unit M)) Unit := do
 let ctx ← read;
diff --git a/tests/lean/run/typeclass_metas_internal_goals1.lean b/tests/lean/run/typeclass_metas_internal_goals1.lean
index 448a1e3a1f..d08fe4451e 100644
--- a/tests/lean/run/typeclass_metas_internal_goals1.lean
+++ b/tests/lean/run/typeclass_metas_internal_goals1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 class Foo (α : Type) : Type := (u : Unit := ())
 class Bar (α : Type) : Type := (u : Unit := ())
diff --git a/tests/lean/run/typeclass_metas_internal_goals2.lean b/tests/lean/run/typeclass_metas_internal_goals2.lean
index dd3f2c46ae..63a6b6198f 100644
--- a/tests/lean/run/typeclass_metas_internal_goals2.lean
+++ b/tests/lean/run/typeclass_metas_internal_goals2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 class Foo (α β : Type) : Type := (u : Unit := ())
 class Bar (α β : Type) : Type := (u : Unit := ())
 class Top : Type := (u : Unit := ())
diff --git a/tests/lean/run/typeclass_metas_internal_goals3.lean b/tests/lean/run/typeclass_metas_internal_goals3.lean
index 8bb076e0bd..1ab0b26caf 100644
--- a/tests/lean/run/typeclass_metas_internal_goals3.lean
+++ b/tests/lean/run/typeclass_metas_internal_goals3.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 class Base (α : Type) := (u:Unit)
 class Depends (α : Type) [Base α] := (u:Unit)
diff --git a/tests/lean/run/typeclass_metas_internal_goals4.lean b/tests/lean/run/typeclass_metas_internal_goals4.lean
index 9246e2aca1..25b7e188cd 100644
--- a/tests/lean/run/typeclass_metas_internal_goals4.lean
+++ b/tests/lean/run/typeclass_metas_internal_goals4.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 class Foo (α β γ : Type) := (u:Unit)
 class Bar (α β γ : Type) := (u:Unit)
 class Top := (u:Unit)
diff --git a/tests/lean/run/typeclass_outparam.lean b/tests/lean/run/typeclass_outparam.lean
index 4606348775..912a3af3b8 100644
--- a/tests/lean/run/typeclass_outparam.lean
+++ b/tests/lean/run/typeclass_outparam.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 class OPClass (α : outParam Type) (β : Type) : Type := (u : Unit := ())
 
diff --git a/tests/lean/run/ubscalar.lean b/tests/lean/run/ubscalar.lean
index 1e65664a01..11dc60fa5b 100644
--- a/tests/lean/run/ubscalar.lean
+++ b/tests/lean/run/ubscalar.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure Foo :=
 (flag : Bool   := false)
diff --git a/tests/lean/run/unexpected_result_with_bind.lean b/tests/lean/run/unexpected_result_with_bind.lean
index 8dccb264d1..c920f2a410 100644
--- a/tests/lean/run/unexpected_result_with_bind.lean
+++ b/tests/lean/run/unexpected_result_with_bind.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 namespace Repro
 
 def FooM (α : Type) : Type := Unit → α
diff --git a/tests/lean/run/unif_issue.lean b/tests/lean/run/unif_issue.lean
index 555c348e5a..3f2d6dc3b2 100644
--- a/tests/lean/run/unif_issue.lean
+++ b/tests/lean/run/unif_issue.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 open Lean
 
 #eval toString $
diff --git a/tests/lean/run/unif_issue2.lean b/tests/lean/run/unif_issue2.lean
index d0e4207177..002b79e79b 100644
--- a/tests/lean/run/unif_issue2.lean
+++ b/tests/lean/run/unif_issue2.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 open Lean
 
diff --git a/tests/lean/sanitizeMacroScopes.lean b/tests/lean/sanitizeMacroScopes.lean
index 01d31aab5b..b3735f0351 100644
--- a/tests/lean/sanitizeMacroScopes.lean
+++ b/tests/lean/sanitizeMacroScopes.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 macro "m" x:term : term => `(fun x => $x)
 
diff --git a/tests/lean/shadow.lean b/tests/lean/shadow.lean
index 3628625f88..06ad2b7328 100644
--- a/tests/lean/shadow.lean
+++ b/tests/lean/shadow.lean
@@ -1,6 +1,6 @@
 import Lean
 
-new_frontend
+
 
 theorem ex1 {α} (x : α) (h : x = x) (x : α) : x = x :=
 h
diff --git a/tests/lean/stdio.lean b/tests/lean/stdio.lean
index 47a77256ff..afb38d9d57 100644
--- a/tests/lean/stdio.lean
+++ b/tests/lean/stdio.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 open IO.FS
 def usingIO {α} (x : IO α) : IO α := x
 
diff --git a/tests/lean/string_imp.lean b/tests/lean/string_imp.lean
index d7a3a86126..9c07cef2b5 100644
--- a/tests/lean/string_imp.lean
+++ b/tests/lean/string_imp.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 #eval ("abc" ++ "cde").length
 #eval ("abcd".mkIterator.nextn 2).remainingToString
 #eval ("abcd".mkIterator.nextn 10).remainingToString
diff --git a/tests/lean/string_imp2.lean b/tests/lean/string_imp2.lean
index 586a8cfd0d..28c75e262d 100644
--- a/tests/lean/string_imp2.lean
+++ b/tests/lean/string_imp2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 def f (s : String) : String :=
 s ++ " " ++ s
 
diff --git a/tests/lean/struct1.lean b/tests/lean/struct1.lean
index fca26b6b34..762bbf7fe9 100644
--- a/tests/lean/struct1.lean
+++ b/tests/lean/struct1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure A (α : Type) :=
 (x : α)
diff --git a/tests/lean/trust0/t1.lean b/tests/lean/trust0/t1.lean
index b5a3732068..c287f20c1f 100644
--- a/tests/lean/trust0/t1.lean
+++ b/tests/lean/trust0/t1.lean
@@ -1,2 +1,2 @@
 import Init.System.IO
-#print trust
+-- #print trust
diff --git a/tests/lean/typeMismatch.lean b/tests/lean/typeMismatch.lean
index e5c53a1fd2..a8e9bdd539 100644
--- a/tests/lean/typeMismatch.lean
+++ b/tests/lean/typeMismatch.lean
@@ -1,5 +1,5 @@
 import Lean
-new_frontend
+
 
 -- Test type mismatch error messages for "liftable" methods
 
diff --git a/tests/lean/typeOf.lean b/tests/lean/typeOf.lean
index d48a7bae57..839936fc63 100644
--- a/tests/lean/typeOf.lean
+++ b/tests/lean/typeOf.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def f1 (x : Nat) (b : Bool) : typeOf! x :=
 let r : typeOf! (x+1) := x+1;
diff --git a/tests/lean/unused_univ.lean b/tests/lean/unused_univ.lean
index 0077e4f3d9..ef4c7e688c 100644
--- a/tests/lean/unused_univ.lean
+++ b/tests/lean/unused_univ.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 variable (y : Nat)
 
diff --git a/tests/lean/zipper.lean b/tests/lean/zipper.lean
index 3ec9be78ec..9c2410cfb1 100644
--- a/tests/lean/zipper.lean
+++ b/tests/lean/zipper.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 structure ListZipper (α : Type) :=
 (xs : List α) (bs : List α)
diff --git a/tests/playground/forIn.lean b/tests/playground/forIn.lean
index 3cc618da7b..544fc1bd59 100644
--- a/tests/playground/forIn.lean
+++ b/tests/playground/forIn.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 namespace ForIn
 
diff --git a/tests/playground/forIn2.lean b/tests/playground/forIn2.lean
index 3850e047fa..f47ca8026d 100644
--- a/tests/playground/forIn2.lean
+++ b/tests/playground/forIn2.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def tst1 : IO Nat :=
 [1, 2, 3, 4, 5, 7, 8, 9, 10, 11, 12, 14].forIn 0 fun a b =>
diff --git a/tests/playground/forthelean/ForTheLean/Demo.lean b/tests/playground/forthelean/ForTheLean/Demo.lean
index 82504a4538..d116a5a624 100644
--- a/tests/playground/forthelean/ForTheLean/Demo.lean
+++ b/tests/playground/forthelean/ForTheLean/Demo.lean
@@ -1,6 +1,6 @@
 -- -*- origami-fold-style: triple-braces -*-
 import ForTheLean.Prelim
-new_frontend
+
 open Lean
 open Lean.Elab.Command
 open Prelim
diff --git a/tests/playground/forthelean/ForTheLean/Prelim.lean b/tests/playground/forthelean/ForTheLean/Prelim.lean
index e58b243338..4c22f1ebd2 100644
--- a/tests/playground/forthelean/ForTheLean/Prelim.lean
+++ b/tests/playground/forthelean/ForTheLean/Prelim.lean
@@ -41,7 +41,7 @@ def wlexem : Parser :=
 try (rawIdent >> checkPrev (fun stx => stx.getId.toString.length > 1 && not ([`is].contains stx.getId)) "")
 end Prelim
 
-new_frontend
+
 open Lean
 open Lean.Elab
 open Lean.Elab.Command
diff --git a/tests/playground/pldi/do1.lean b/tests/playground/pldi/do1.lean
index 426f0ffa14..ec6a468cad 100644
--- a/tests/playground/pldi/do1.lean
+++ b/tests/playground/pldi/do1.lean
@@ -1,4 +1,4 @@
-new_frontend
+
 
 def getVal : IO Nat :=
 IO.rand 0 100
diff --git a/tests/playground/pldi/do2.lean b/tests/playground/pldi/do2.lean
index 979622c9b7..ebba3165db 100644
--- a/tests/playground/pldi/do2.lean
+++ b/tests/playground/pldi/do2.lean
@@ -22,7 +22,7 @@ fun stx => do
   if expanded then pure stx
   else Macro.throwUnsupported
 
-new_frontend
+
 
 syntax:max [doHash] "#" : term
 
diff --git a/tests/playground/webserver/Webserver.lean b/tests/playground/webserver/Webserver.lean
index 13bc0569ca..71e716b6b5 100644
--- a/tests/playground/webserver/Webserver.lean
+++ b/tests/playground/webserver/Webserver.lean
@@ -85,7 +85,7 @@ partial def run : IO.FS.Handle → IO.FS.Handle → IO Unit
 end Webserver
 --}}}
 
-new_frontend
+
 open Lean
 open Lean.Parser