From 95efa3dcd262d859ee34f6aed7c694cb8d2acf9a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 29 Jun 2022 15:35:34 -0700
Subject: [PATCH] fix: `withPosition` case at `MacroArgUtil`

fixes #1267 after update stage0
---
 src/Lean/Elab/MacroArgUtil.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean
index 2e516134f8..6b051e4dd3 100644
--- a/src/Lean/Elab/MacroArgUtil.lean
+++ b/src/Lean/Elab/MacroArgUtil.lean
@@ -33,7 +33,9 @@ where
     | `(stx| interpolatedStr(term)) => pure ⟨Syntax.mkAntiquotNode interpolatedStrKind id⟩
     -- bind through withPosition
     | `(stx| withPosition($stx)) =>
-      return (← mkSyntaxAndPat id? id stx)
+      let (stx, pat) ← mkSyntaxAndPat id? id stx
+      let stx ← `(stx| withPosition($stx))
+      return (stx, pat)
     | _ => match id? with
       -- if there is a binding, we assume the user knows what they are doing
       | some id => mkAntiquotNode stx id