fix: elaborating category quotations

src/Lean/Elab/Quotation.lean

@@ -177,6 +177,7 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
   | k => throwError "unexpected quotation kind {k}"
 
 def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do
+  let stx := if stx.getNumArgs == 1 then stx[0] else stx
   /- Syntax quotations are monadic values depending on the current macro scope. For efficiency, we bind
      the macro scope once for each quotation, then build the syntax tree in a completely pure computation
      depending on this binding. Note that regular function calls do not introduce a new macro scope (i.e.

src/Lean/Elab/Syntax.lean

@@ -221,11 +221,12 @@ private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := d
     let name := catName ++ `quot
     let cmd ← `(
       @[termParser] def $(mkIdent name) : Lean.ParserDescr :=
-        Lean.ParserDescr.node $(quote name) $(quote Lean.Parser.maxPrec)
-          (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
-            (Lean.ParserDescr.binary `andthen
-              (Lean.ParserDescr.cat $(quote catName) 0)
-              (Lean.ParserDescr.symbol ")"))))
+        Lean.ParserDescr.node `Lean.Parser.Term.quot $(quote Lean.Parser.maxPrec)
+          (Lean.ParserDescr.node $(quote name) $(quote Lean.Parser.maxPrec)
+            (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol $(quote quotSymbol))
+              (Lean.ParserDescr.binary `andthen
+                (Lean.ParserDescr.cat $(quote catName) 0)
+                (Lean.ParserDescr.symbol ")")))))
     elabCommand cmd
 
 @[builtinCommandElab syntaxCat] def elabDeclareSyntaxCat : CommandElab := fun stx => do

src/Lean/Syntax.lean

@@ -372,6 +372,7 @@ def isQuot : Syntax → Bool
   | _                                             => false
 
 def getQuotContent (stx : Syntax) : Syntax :=
+  let stx := if stx.getNumArgs == 1 then stx[0] else stx
   if stx.isOfKind `Lean.Parser.Term.dynamicQuot then
     stx[3]
   else