From df49512880fdc6fc263bb83fefe4fe923047e9f0 Mon Sep 17 00:00:00 2001
From: Mario Carneiro <di.gama@gmail.com>
Date: Wed, 17 May 2023 02:47:18 -0400
Subject: [PATCH] fix: use withoutPosition in anon constructor

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

diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index b30445ea6a..e84cfb32a0 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -158,7 +158,7 @@ are turned into a new anonymous constructor application. For example,
 `⟨a, b, c⟩ : α × (β × γ)` is equivalent to `⟨a, ⟨b, c⟩⟩`.
 -/
 @[builtin_term_parser] def anonymousCtor := leading_parser
-  "⟨" >> sepBy termParser ", " >> "⟩"
+  "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", ")) >> "⟩"
 def optIdent : Parser :=
   optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser