From d379cd6853601399e271b2b875c2d13236342925 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 15 Oct 2021 19:40:09 +0200
Subject: [PATCH] fix: out-of-bounds array access

---
 src/Lean/Elab/Syntax.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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