From 8d021e0cec16cd7956475b4ba7b289281e395af2 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 9 Jan 2020 12:36:18 -0500
Subject: [PATCH] fix: fresh macro scope per command

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

diff --git a/src/Init/Lean/Elab/Command.lean b/src/Init/Lean/Elab/Command.lean
index 0a42b3ae52..7ec695021d 100644
--- a/src/Init/Lean/Elab/Command.lean
+++ b/src/Init/Lean/Elab/Command.lean
@@ -197,7 +197,7 @@ private def elabCommandUsing (stx : Syntax) : List CommandElab → CommandElabM
     | Exception.unsupportedSyntax => elabCommandUsing elabFns)
 
 def elabCommandAux (stx : Syntax) : CommandElabM Unit :=
-withIncRecDepth stx $ match stx with
+withIncRecDepth stx $ withFreshMacroScope $ match stx with
 | Syntax.node _ _ => do
   s ← get;
   let table := (commandElabAttribute.ext.getState s.env).table;