diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 5b74d6f5af..dff8715692 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -342,8 +342,7 @@ def checkRuleKind (given expected : SyntaxNodeKind) : Bool :=
   given == expected || given == expected ++ `antiquot
 
 def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
-  | `(matchAltExpr| | $pats,* => $rhs) => do
-    let pat := pats.elemsAndSeps[0]
+  | `(matchAltExpr| | $pat:term => $rhs) => do
     if !pat.isQuot then
       throwUnsupportedSyntax
     let quoted := getQuotContent pat