From 3b34a150ffad6231f485b0ba4ecd726b63b70a67 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 14 Oct 2020 17:30:26 -0700
Subject: [PATCH] chore: use `#lang lean4`

---
 src/Lean/Elab/App.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 399346435f..aaa616e497 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.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.
@@ -7,7 +8,6 @@ import Lean.Util.FindMVar
 import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.SyntheticMVars
-new_frontend
 
 namespace Lean.Elab.Term
 open Meta