diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index f50d14cb67..35ff8dbce7 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -131,7 +131,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax
           let arr ← match k with
             | `optional => `(match $[$ids:ident],* with
                 | $[some $ids:ident],* => $(quote inner)
-                | none                 => Array.empty)
+                | $[_%$ids],*          => Array.empty)
             | _ =>
               let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back
               `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr)
diff --git a/tests/lean/run/1124.lean b/tests/lean/run/1124.lean
new file mode 100644
index 0000000000..a344a16aa1
--- /dev/null
+++ b/tests/lean/run/1124.lean
@@ -0,0 +1,5 @@
+open Lean
+syntax "foo" (ident ident)? : term
+
+variable (x y : Option Syntax)
+example : MacroM Syntax := `(foo $[$x:ident $y:ident]?)