diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean
index 7e259170d2..e3d72608e0 100644
--- a/src/Init/Lean/Elab/Quotation.lean
+++ b/src/Init/Lean/Elab/Quotation.lean
@@ -330,8 +330,11 @@ alts ← alts.getArgs.getSepElems.mapM $ fun alt => do {
   pat ← if pats.getArgs.size == 1 then pure $ pats.getArg 0
     else throwError stx "match_syntax: expected exactly one pattern per alternative";
   let pat := if pat.isOfKind `Lean.Parser.Term.stxQuot then pat.setArg 1 $ elimAntiquotChoices $ pat.getArg 1 else pat;
-  let rhs := alt.getArg 2;
-  pure ([pat], rhs)
+  match pat.find? $ fun stx => stx.getKind == choiceKind with
+  | some choiceStx => throwError choiceStx "invalid pattern, nested syntax has multiple interpretations"
+  | none           =>
+    let rhs := alt.getArg 2;
+    pure ([pat], rhs)
 };
 -- letBindRhss (compileStxMatch stx [discr]) alts.toList []
 compileStxMatch stx [discr] alts.toList
diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean
index 5820bac15e..2e477a29b6 100644
--- a/src/Init/LeanInit.lean
+++ b/src/Init/LeanInit.lean
@@ -750,6 +750,13 @@ match stx.isTermId? relaxed with
 | some (id, opt) => if opt.isNone then some id else none
 | none           => none
 
+partial def findAux (p : Syntax → Bool) : Syntax → Option Syntax
+| stx@(Syntax.node _ args) => if p stx then some stx else args.findSome? findAux
+| stx                      => if p stx then some stx else none
+
+def find? (stx : Syntax) (p : Syntax → Bool) : Option Syntax :=
+findAux p stx
+
 end Syntax
 end Lean