From 3c86f79bad9eba75d63b690be07cf50fcb340ea3 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Wed, 25 Nov 2020 20:25:43 +0100
Subject: [PATCH] fix: one instance of parenthesizer "visiting a syntax tree
 without precedences"

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

diff --git a/src/Lean/Parser/Basic.lean b/src/Lean/Parser/Basic.lean
index 701056db99..5c06d22470 100644
--- a/src/Lean/Parser/Basic.lean
+++ b/src/Lean/Parser/Basic.lean
@@ -1555,7 +1555,7 @@ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true
   -- antiquotation kind via `noImmediateColon`
   let nameP := if anonymous then nameP <|> checkNoImmediateColon >> pushNone else nameP
   -- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error
-  node kind $ atomic $
+  leadingNode kind maxPrec $ atomic $
     setExpected [] "$" >>
     many (checkNoWsBefore "" >> "$") >>
     checkNoWsBefore "no space before spliced term" >> antiquotExpr >>