diff --git a/src/Init/Lean/Elab/Term.lean b/src/Init/Lean/Elab/Term.lean
index bb146e1ce7..77f93b50f1 100644
--- a/src/Init/Lean/Elab/Term.lean
+++ b/src/Init/Lean/Elab/Term.lean
@@ -24,7 +24,7 @@ structure Context extends Meta.Context :=
 (univNames       : List Name       := [])
 (openDecls       : List OpenDecl   := [])
 (macroStack      : List Syntax     := [])
-(macroScopeStack : List MacroScope := [0])
+(currMacroScope  : MacroScope := 0)
 /- When `mayPostpone == true`, an elaboration function may interrupt its execution by throwing `Exception.postpone`.
    The function `elabTerm` catches this exception and creates fresh synthetic metavariable `?m`, stores `?m` in
    the list of pending synthetic metavariables, and returns `?m`. -/
@@ -109,11 +109,11 @@ throw (Exception.error msg)
 
 protected def getCurrMacroScope : TermElabM Nat := do
 ctx ← read;
-pure ctx.macroScopeStack.head!
+pure ctx.currMacroScope
 
 @[inline] protected def withFreshMacroScope {α} (x : TermElabM α) : TermElabM α := do
 fresh ← modifyGet (fun st => (st.nextMacroScope, { st with nextMacroScope := st.nextMacroScope + 1 }));
-adaptReader (fun (ctx : Context) => { ctx with macroScopeStack := fresh::ctx.macroScopeStack }) x
+adaptReader (fun (ctx : Context) => { ctx with currMacroScope := fresh }) x
 
 instance TermElabM.MonadQuotation : MonadQuotation TermElabM := {
   getCurrMacroScope   := Term.getCurrMacroScope,
diff --git a/src/Init/Lean/Hygiene.lean b/src/Init/Lean/Hygiene.lean
index dcafcb45ac..5c10103bf4 100644
--- a/src/Init/Lean/Hygiene.lean
+++ b/src/Init/Lean/Hygiene.lean
@@ -55,17 +55,15 @@ mkNameNum n scp
     processing of a file). It uses the state monad to query and allocate the
     next macro scope, and uses the reader monad to store the stack of scopes
     corresponding to `withFreshMacroScope` calls. -/
-abbrev Unhygienic := ReaderT (List Nat) $ StateM Nat
+abbrev Unhygienic := ReaderT MacroScope $ StateM MacroScope
 namespace Unhygienic
 instance MonadQuotation : MonadQuotation Unhygienic := {
-  getCurrMacroScope := do
-    stack ← read;
-    pure stack.head!,
+  getCurrMacroScope := read,
   withFreshMacroScope := fun α x => do
     fresh ← modifyGet (fun n => (n, n + 1));
-    adaptReader (fun stack => fresh::stack) x
+    adaptReader (fun _ => fresh) x
 }
-protected def run {α : Type} (x : Unhygienic α) : α := run x [0] 1
+protected def run {α : Type} (x : Unhygienic α) : α := run x 0 1
 end Unhygienic
 
 instance monadQuotationTrans {m n : Type → Type} [MonadQuotation m] [HasMonadLift m n] [MonadFunctorT m m n n] : MonadQuotation n :=