diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index a5eab247c5..f93716a1d4 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/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.
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index b199b46678..13cedcb80c 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/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
diff --git a/src/Lean/Syntax.lean b/src/Lean/Syntax.lean
index 309a609f96..221e490ee4 100644
--- a/src/Lean/Syntax.lean
+++ b/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