diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 8927554d00..f50d14cb67 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -194,6 +194,7 @@ elab_stx_quot Parser.Term.attr.quot
 elab_stx_quot Parser.Term.prio.quot
 elab_stx_quot Parser.Term.doElem.quot
 elab_stx_quot Parser.Term.dynamicQuot
+elab_stx_quot Parser.Command.quot
 
 /- match -/
 
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index e6f0df3c62..b85e1558d6 100644
--- a/src/Lean/Parser/Command.lean
+++ b/src/Lean/Parser/Command.lean
@@ -9,17 +9,19 @@ import Lean.Parser.Do
 namespace Lean
 namespace Parser
 
-/--
-  Syntax quotation for terms and (lists of) commands. We prefer terms, so ambiguous quotations like
-  `` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
-  Multiple command will be put in a `` `null `` node, but a single command will not (so that you can directly
-  match against a quotation in a command kind's elaborator). -/
--- TODO: use two separate quotation parsers with parser priorities instead
-@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth (termParser <|> many1Unbox commandParser) >> ")"
+/-- Syntax quotation for terms. -/
+@[builtinTermParser] def Term.quot := leading_parser "`(" >> incQuotDepth termParser >> ")"
 @[builtinTermParser] def Term.precheckedQuot := leading_parser "`" >> Term.quot
 
 namespace Command
 
+/--
+  Syntax quotation for (sequences of) commands. The identical syntax for term quotations takes priority, so ambiguous quotations like
+  `` `($x $y) `` will be parsed as an application, not two commands. Use `` `($x:command $y:command) `` instead.
+  Multiple commands will be put in a `` `null `` node, but a single command will not (so that you can directly
+  match against a quotation in a command kind's elaborator). -/
+@[builtinTermParser low] def quot := leading_parser "`(" >> incQuotDepth (many1Unbox commandParser) >> ")"
+
 /--
   A mutual block may be broken in different cliques, we identify them using an `ident` (an element of the clique)
   We provide two kinds of hints to the termination checker:
diff --git a/tests/lean/StxQuot.lean.expected.out b/tests/lean/StxQuot.lean.expected.out
index da6a5d841a..cc50beb9a7 100644
--- a/tests/lean/StxQuot.lean.expected.out
+++ b/tests/lean/StxQuot.lean.expected.out
@@ -1,4 +1,4 @@
-StxQuot.lean:8:12: error: expected command, identifier or term
+StxQuot.lean:8:12: error: expected identifier or term
 "`Nat.one._@.UnhygienicMain._hyg.1"
 "<missing>"
 "<missing>"