From d1dcf0b0675e6bc614a90f7d758de92becab1a20 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Fri, 23 Apr 2021 18:02:50 -0700
Subject: [PATCH] chore: cleanup

We still need another update stage0
---
 src/Init/Prelude.lean   | 17 +----------------
 src/Lean/Elab/Util.lean | 14 ++++++++------
 2 files changed, 9 insertions(+), 22 deletions(-)

diff --git a/src/Init/Prelude.lean b/src/Init/Prelude.lean
index b348496ba5..b42dcb0e84 100644
--- a/src/Init/Prelude.lean
+++ b/src/Init/Prelude.lean
@@ -2114,24 +2114,9 @@ unsafe def getMethodsImp : MacroM Methods :=
 
 @[implementedBy getMethodsImp] constant getMethods : MacroM Methods
 
-structure MethodsOld where
-  expandMacro?     : Syntax → MacroM (Option Syntax)
-  deriving Inhabited
-
-unsafe def mkMethodsOldImp (descr : MethodsOld) : MethodsRef :=
-  unsafeCast descr
-
-@[implementedBy mkMethodsOldImp]
-constant mkMethodsOld (descr : MethodsOld) : MethodsRef
-
-unsafe def getMethodsOldImp : MacroM MethodsOld :=
-  bind read fun ctx => pure (unsafeCast (ctx.methodsOld))
-
-@[implementedBy getMethodsOldImp] constant getMethodsOld : MacroM MethodsOld
-
 /-- `expandMacro? stx` return `some stxNew` if `stx` is a macro, and `stxNew` is its expansion. -/
 def expandMacro? (stx : Syntax) : MacroM (Option Syntax) := do
-  (← getMethodsOld).expandMacro? stx
+  (← getMethods).expandMacro? stx
 
 /-- Return `true` if the environment contains a declaration with name `declName` -/
 def hasDecl (declName : Name) : MacroM Bool := do
diff --git a/src/Lean/Elab/Util.lean b/src/Lean/Elab/Util.lean
index aaf2f584ca..0ca8fe0c37 100644
--- a/src/Lean/Elab/Util.lean
+++ b/src/Lean/Elab/Util.lean
@@ -157,17 +157,19 @@ private def expandMacro? (env : Environment) (stx : Syntax) : MacroM (Option Syn
 @[inline] def liftMacroM {α} {m : Type → Type} [Monad m] [MonadMacroAdapter m] [MonadEnv m] [MonadRecDepth m] [MonadError m] [MonadResolveName m] (x : MacroM α) : m α := do
   let env  ← getEnv
   let currNamespace ← getCurrNamespace
-  match x { methodsOld     := Macro.mkMethodsOld { expandMacro? := expandMacro? env }
+  let methods := Macro.mkMethods {
+    expandMacro?     := expandMacro? env
+    hasDecl          := fun declName => return env.contains declName
+    getCurrNamespace := return currNamespace
+  }
+  match x { methodsOld     := methods
             ref            := ← getRef
             currMacroScope := ← MonadMacroAdapter.getCurrMacroScope
             mainModule     := env.mainModule
             currRecDepth   := ← MonadRecDepth.getRecDepth
             maxRecDepth    := ← MonadRecDepth.getMaxRecDepth
-            methods        := Macro.mkMethods {
-              expandMacro?     := expandMacro? env
-              hasDecl          := fun declName => return env.contains declName
-              getCurrNamespace := return currNamespace
-            } }
+            methods        := methods
+          }
           { macroScope := (← MonadMacroAdapter.getNextMacroScope), extra := arbitrary } with
   | EStateM.Result.error Macro.Exception.unsupportedSyntax _ => throwUnsupportedSyntax
   | EStateM.Result.error (Macro.Exception.error ref msg) _   => throwErrorAt ref msg