diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean
index 556c07edb7..c7210122a3 100644
--- a/src/Lean/Elab/Binders.lean
+++ b/src/Lean/Elab/Binders.lean
@@ -4,9 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 import Lean.Elab.Term
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term
 open Meta
+open Lean.Parser.Term
 
 /--
   Given syntax of the forms
@@ -350,10 +352,11 @@ def elabFunBinders {α} (binders : Array Syntax) (expectedType? : Option Expr) (
       x s.fvars s.expectedType?
 
 /- Helper function for `expandEqnsIntoMatch` -/
-private def getMatchAltNumPatterns (matchAlts : Syntax) : Nat :=
-  let alt0 := matchAlts[1][0]
-  let pats := alt0[0].getSepArgs
-  pats.size
+private def getMatchAltsNumPatterns : Syntax → Nat
+  | alts => match alts[0][0] with
+    | `(matchAltExpr| | $pats,* => $rhs) =>
+      pats.getElems.size
+    | _ => unreachable!
 
 private def mkMatch (ref : Syntax) (discrs : Array Syntax) (matchAlts : Syntax) (matchTactic := false) : Syntax :=
   Syntax.node (if matchTactic then `Lean.Parser.Tactic.match else `Lean.Parser.Term.match)
@@ -429,10 +432,10 @@ private def expandMatchAltsIntoMatchAux (ref : Syntax) (matchAlts : Syntax) (mat
     ```
  -/
 def expandMatchAltsIntoMatch (ref : Syntax) (matchAlts : Syntax) (tactic := false) : MacroM Syntax :=
-  expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltNumPatterns matchAlts) #[]
+  expandMatchAltsIntoMatchAux ref matchAlts tactic (getMatchAltsNumPatterns matchAlts) #[]
 
 def expandMatchAltsIntoMatchTactic (ref : Syntax) (matchAlts : Syntax) : MacroM Syntax :=
-  expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltNumPatterns matchAlts) #[]
+  expandMatchAltsIntoMatchAux ref matchAlts true (getMatchAltsNumPatterns matchAlts) #[]
 
 /--
   Similar to `expandMatchAltsIntoMatch`, but supports an optional `where` clause.
@@ -477,7 +480,7 @@ def expandMatchAltsWhereDecls (ref : Syntax) (matchAltsWhereDecls : Syntax) : Ma
       let x ← `(x)
       let body ← loop n (addDiscr ref discrs x)
       `(@fun $x => $body)
-  loop (getMatchAltNumPatterns matchAlts) #[]
+  loop (getMatchAltsNumPatterns matchAlts) #[]
 
 @[builtinTermElab «fun»] def elabFun : TermElab := fun stx expectedType? => match stx with
   | `(fun $binders* => $body) => do
diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean
index 155634f766..ff59524da0 100644
--- a/src/Lean/Elab/Deriving/BEq.lean
+++ b/src/Lean/Elab/Deriving/BEq.lean
@@ -8,7 +8,7 @@ import Lean.Elab.Deriving.Basic
 import Lean.Elab.Deriving.Util
 
 namespace Lean.Elab.Deriving.BEq
-
+open Lean.Parser.Term
 open Meta
 
 structure Header where
@@ -37,7 +37,7 @@ def mkHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
 def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) (argNames : Array Name) : TermElabM Syntax := do
   let discrs ← mkDiscrs
   let alts ← mkAlts
-  `(match $[$discrs],* with | $[$alts:matchAlt]|*)
+  `(match $[$discrs],* with $alts:matchAlt*)
 where
   mkDiscr (varName : Name) : TermElabM Syntax :=
     `(Parser.Term.matchDiscr| $(mkIdent varName):term)
@@ -57,7 +57,7 @@ where
     patterns := patterns.push (← `(_))
     patterns := patterns.push (← `(_))
     let altRhs ← `(false)
-    `(matchAltExpr| $[$patterns:term],* => $altRhs:term)
+    `(matchAltExpr| | $[$patterns:term],* => $altRhs:term)
 
   mkAlts : TermElabM (Array Syntax) := do
     let mut alts := #[]
@@ -93,7 +93,7 @@ where
               rhs ← `($rhs && $a:ident == $b:ident)
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs1:term*))
         patterns := patterns.push (← `(@$(mkIdent ctorName):ident $ctorArgs2:term*))
-        `(matchAltExpr| $[$patterns:term],* => $rhs:term)
+        `(matchAltExpr| | $[$patterns:term],* => $rhs:term)
       alts := alts.push alt
     alts := alts.push (← mkElseAlt)
     return alts
diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean
index c4fb1e68da..c014489711 100644
--- a/src/Lean/Elab/Deriving/Util.lean
+++ b/src/Lean/Elab/Deriving/Util.lean
@@ -12,7 +12,6 @@ open Meta
 def implicitBinderF := Parser.Term.implicitBinder
 def instBinderF     := Parser.Term.instBinder
 def explicitBinderF := Parser.Term.explicitBinder
-def matchAltExpr    := Parser.Term.matchAlt
 
 def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do
   forallTelescopeReducing indVal.type fun xs _ => do
diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean
index 1d1ebc5be8..67c97a58b0 100644
--- a/src/Lean/Elab/Do.lean
+++ b/src/Lean/Elab/Do.lean
@@ -7,6 +7,7 @@ import Lean.Elab.Term
 import Lean.Elab.Binders
 import Lean.Elab.Match
 import Lean.Elab.Quotation.Util
+import Lean.Parser.Do
 
 namespace Lean.Elab.Term
 open Meta
@@ -1016,15 +1017,12 @@ partial def toTerm : Code → M Syntax
   | Code.seq stx k          => do seqToTerm stx (← toTerm k)
   | Code.ite ref _ o c t e  => do mkIte ref o c (← toTerm t) (← toTerm e)
   | Code.«match» ref discrs optType alts => do
-    let mut termSepAlts := #[]
+    let mut termAlts := #[]
     for alt in alts do
-      termSepAlts := termSepAlts.push $ mkAtomFrom alt.ref "|"
       let rhs ← toTerm alt.rhs
-      let termAlt  := mkNode `Lean.Parser.Term.matchAlt #[alt.patterns, mkAtomFrom alt.ref "=>", rhs]
-      termSepAlts := termSepAlts.push termAlt
-    let firstVBar     := termSepAlts[0]
-    let termSepAlts   := mkNullNode termSepAlts[1:termSepAlts.size]
-    let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode #[firstVBar], termSepAlts]
+      let termAlt := mkNode `Lean.Parser.Term.matchAlt #[mkAtomFrom alt.ref "|", alt.patterns, mkAtomFrom alt.ref "=>", rhs]
+      termAlts := termAlts.push termAlt
+    let termMatchAlts := mkNode `Lean.Parser.Term.matchAlts #[mkNullNode termAlts]
     pure $ mkNode `Lean.Parser.Term.«match» #[mkAtomFrom ref "match", discrs, optType, mkAtomFrom ref "with", termMatchAlts]
 
 def run (code : Code) (m : Syntax) (uvars : Array Name := #[]) (kind := Kind.regular) : MacroM Syntax := do
@@ -1328,22 +1326,16 @@ def doForToCode (doSeqToCode : List Syntax → M CodeBlock) (doFor : Syntax) (do
       let auxDo ← `(do let r ← $forInTerm:term; $uvarsTuple:term := r)
       doSeqToCode (getDoSeqElems (getDoSeq auxDo) ++ doElems)
 
-/--
-  Generate `CodeBlock` for `doMatch; doElems`
-  ```
-  def doMatchAlt   := sepBy1 termParser ", " >> darrow >> doSeq
-  def doMatchAlts  := parser! optional "| " >> sepBy1 doMatchAlt "|"
-  def doMatch      := parser! "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> doMatchAlts
-  ``` -/
+/-- Generate `CodeBlock` for `doMatch; doElems` -/
 def doMatchToCode (doSeqToCode : List Syntax → M CodeBlock) (doMatch : Syntax) (doElems: List Syntax) : M CodeBlock := do
   let ref       := doMatch
   let discrs    := doMatch[1]
   let optType   := doMatch[2]
-  let matchAlts := doMatch[4][1].getSepArgs -- Array of `doMatchAlt`
+  let matchAlts := doMatch[4][0].getArgs -- Array of `doMatchAlt`
   let alts ←  matchAlts.mapM fun matchAlt => do
-    let patterns := matchAlt[0]
+    let patterns := matchAlt[1]
     let vars ← getPatternsVarsEx patterns.getSepArgs
-    let rhs  := matchAlt[2]
+    let rhs  := matchAlt[3]
     let rhs ← doSeqToCode (getDoSeqElems rhs)
     pure { ref := matchAlt, vars := vars, patterns := patterns, rhs := rhs : Alt CodeBlock }
   let matchCode ← mkMatch ref discrs optType alts
diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean
index d9b9118cb1..43cef0a4c9 100644
--- a/src/Lean/Elab/Match.lean
+++ b/src/Lean/Elab/Match.lean
@@ -7,6 +7,7 @@ import Lean.Meta.Match.MatchPatternAttr
 import Lean.Meta.Match.Match
 import Lean.Elab.SyntheticMVars
 import Lean.Elab.App
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term
 open Meta
@@ -14,15 +15,6 @@ open Meta
 /- This modules assumes "match"-expressions use the following syntax.
 
 ```lean
-def matchAlt : Parser :=
-nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
-  sepBy1 termParser ", " >> darrow >> termParser
-
-def matchAlts (optionalFirstBar := true) : Parser :=
-group $ withPosition $ fun pos =>
-  (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
-
 def matchDiscr := parser! optional (try (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
 
 def «match» := parser!:leadPrec "match " >> sepBy1 matchDiscr ", " >> optType >> " with " >> matchAlts
@@ -34,12 +26,6 @@ structure MatchAltView where
   patterns : Array Syntax
   rhs      : Syntax
 
-def mkMatchAltView (ref : Syntax) (matchAlt : Syntax) : MatchAltView := {
-  ref      := ref
-  patterns := matchAlt[0].getSepArgs
-  rhs      := matchAlt[2]
-}
-
 private def expandSimpleMatch (stx discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do
   let newStx ← `(let $lhsVar := $discr; $rhs)
   withMacroExpansion stx newStx $ elabTerm newStx expectedType?
@@ -122,28 +108,20 @@ private def elabMatchTypeAndDiscrs (discrStxs : Array Syntax) (matchOptType : Sy
     let discrs ← elabDiscrsWitMatchType discrStxs matchType expectedType
     pure (discrs, matchType, matchAltViews)
 
-/-
-nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $ sepBy1 termParser ", " >> darrow >> termParser
--/
 def expandMacrosInPatterns (matchAlts : Array MatchAltView) : MacroM (Array MatchAltView) := do
   matchAlts.mapM fun matchAlt => do
     let patterns ← matchAlt.patterns.mapM expandMacros
     pure { matchAlt with patterns := patterns }
 
-  /- Given `stx` a match-expression, return its alternatives. -/
-  private def getMatchAlts (stx : Syntax) : Array MatchAltView := do
-  let matchAlts  := stx[4]
-  let firstVBar  := matchAlts[0]
-  let mut ref    := firstVBar
-  let mut result := #[]
-  for arg in matchAlts[1].getArgs do
-    if ref.isNone then
-      ref := arg -- The first vertical bar is optional
-    if arg.getKind == `Lean.Parser.Term.matchAlt then
-      result := result.push (mkMatchAltView ref arg)
-    else
-      ref := arg -- current `arg` is a vertical bar
-  pure result
+/- Given `stx` a match-expression, return its alternatives. -/
+private def getMatchAlts : Syntax → Array MatchAltView
+  | `(match $discrs,* $[: $ty?]? with $[| $patternss,* => $rhss]*) =>
+    patternss.zipWith rhss fun patterns rhs => {
+      ref      := patterns[0],
+      patterns := patterns,
+      rhs      := rhs
+    }
+  | stx => dbgTrace s!"{stx}" fun _ => unreachable!
 
 /--
   Auxiliary annotation used to mark terms marked with the "inaccessible" annotation `.(t)` and
@@ -894,9 +872,7 @@ private def elabMatchCore (stx : Syntax) (expectedType? : Option Expr) : TermEla
 -- parser! "match " >> sepBy1 termParser ", " >> optType >> " with " >> matchAlts
 @[builtinTermElab «match»] def elabMatch : TermElab := fun stx expectedType? =>
   match stx with
-  | `(match $discr:term with $y:ident => $rhs:term)           => expandSimpleMatch stx discr y rhs expectedType?
   | `(match $discr:term with | $y:ident => $rhs:term)         => expandSimpleMatch stx discr y rhs expectedType?
-  | `(match $discr:term : $type with $y:ident => $rhs:term)   => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | `(match $discr:term : $type with | $y:ident => $rhs:term) => expandSimpleMatchWithType stx discr y type rhs expectedType?
   | _ => do
     match (← expandNonAtomicDiscrs? stx) with
diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean
index 15c8ba2eac..3a62ad9ccc 100644
--- a/src/Lean/Elab/MutualDef.lean
+++ b/src/Lean/Elab/MutualDef.lean
@@ -166,10 +166,6 @@ private def expandWhereDeclsAsStructInst (whereDecls : Syntax) : MacroM Syntax :
 /-
 Recall that
 ```
-def matchAlts (optionalFirstBar := true) : Parser :=
-withPosition $ fun pos =>
-  (if optionalFirstBar then optional "| " else "| ") >>
-  sepBy1 matchAlt (checkColGe pos.column "alternatives must be indented" >> "|")
 def declValSimple    := parser! " :=\n" >> termParser >> optional Term.whereDecls
 def declValEqns      := parser! Term.matchAltsWhereDecls
 def declVal          := declValSimple <|> declValEqns <|> Term.whereDecls
diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean
index 4d28bc59df..cd00890d32 100644
--- a/src/Lean/Elab/Quotation.lean
+++ b/src/Lean/Elab/Quotation.lean
@@ -10,6 +10,7 @@ import Lean.Syntax
 import Lean.ResolveName
 import Lean.Elab.Term
 import Lean.Elab.Quotation.Util
+import Lean.Parser.Term
 
 namespace Lean.Elab.Term.Quotation
 
@@ -343,7 +344,7 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li
 
 def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do
   match stx with
-  | `(match $[$discrs:term],* with $[|]? $[$[$patss],* => $rhss]|*) => do
+  | `(match $[$discrs:term],* with $[| $[$patss],* => $rhss]*) => do
     -- letBindRhss ...
     if patss.all (·.all (!·.isQuot)) then
       -- no quotations => fall back to regular `match`
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index 7e027d20ed..7fbfe86699 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -172,6 +172,7 @@ end Term
 
 namespace Command
 open Lean.Syntax
+open Lean.Parser.Term hiding macroArg
 open Lean.Parser.Command
 
 private def getCatSuffix (catName : Name) : String :=
@@ -329,54 +330,56 @@ def syntaxAbbrev  := parser! "syntax " >> ident >> " := " >> many1 syntaxParser
   Recall that syntax node kinds contain the current namespace.
 -/
 def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do
-  let alts ← alts.mapSepElemsM fun alt => do
-    let lhs := alt[0]
-    let pat := lhs[0]
+  let alts ← alts.mapM fun alt => match alt with
+    | `(matchAltExpr| | $pats,* => $rhs) => do
+      let pat := pats.elemsAndSeps[0]
+      if !pat.isQuot then
+        throwUnsupportedSyntax
+      let quoted := getQuotContent pat
+      let k' := quoted.getKind
+      if k' == k then
+        pure alt
+      else if k' == choiceKind then
+         match quoted.getArgs.find? fun quotAlt => quotAlt.getKind == k with
+         | none        => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
+         | some quoted =>
+           let pat := pat.setArg 1 quoted
+           let pats := pats.elemsAndSeps.set! 0 pat
+           `(matchAltExpr| | $pats,* => $rhs)
+      else
+        throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
+    | _ => throwUnsupportedSyntax
+  `(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
+     fun $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
+
+def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind
+  | `(matchAltExpr| | $pats,* => $rhs) => do
+    let pat := pats.elemsAndSeps[0]
     if !pat.isQuot then
       throwUnsupportedSyntax
-    let quot := pat[1]
-    let k' := quot.getKind
-    if k' == k then
-      pure alt
-    else if k' == choiceKind then
-       match quot.getArgs.find? fun quotAlt => quotAlt.getKind == k with
-       | none      => throwErrorAt! alt "invalid macro_rules alternative, expected syntax node kind '{k}'"
-       | some quot =>
-         let pat := pat.setArg 1 quot
-         let lhs := lhs.setArg 0 pat
-         pure $ alt.setArg 0 lhs
-    else
-      throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
-  `(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
-     fun | $(SepArray.mk alts):matchAlt|* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
-
-def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
-  let lhs := alt[0]
-  let pat := lhs[0]
-  if !pat.isQuot then
-    throwUnsupportedSyntax
-  let quot := pat[1]
-  pure quot.getKind
+    let quoted := getQuotContent pat
+    pure quoted.getKind
+  | _ => throwUnsupportedSyntax
 
 def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
-  let k ← inferMacroRulesAltKind (alts.get! 0)
+  let k ← inferMacroRulesAltKind alts[0]
   if k == choiceKind then
     throwErrorAt! alts[0]
       "invalid macro_rules alternative, multiple interpretations for pattern (solution: specify node kind using `macro_rules [<kind>] ...`)"
   else
-    let altsK    ← alts.filterSepElemsM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
-    let altsNotK ← alts.filterSepElemsM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
+    let altsK    ← alts.filterM fun alt => do pure $ k == (← inferMacroRulesAltKind alt)
+    let altsNotK ← alts.filterM fun alt => do pure $ k != (← inferMacroRulesAltKind alt)
     let defCmd   ← elabMacroRulesAux k altsK
     if altsNotK.isEmpty then
       pure defCmd
     else
-      `($defCmd:command macro_rules $(SepArray.mk altsNotK):matchAlt|*)
+      `($defCmd:command macro_rules $altsNotK:matchAlt*)
 
 @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
   adaptExpander fun stx => match stx with
-  | `(macro_rules $[|]? $alts:matchAlt|*)         => elabNoKindMacroRulesAux alts.elemsAndSeps
-  | `(macro_rules [$kind] $[|]? $alts:matchAlt|*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts.elemsAndSeps
-  | _                                             => throwUnsupportedSyntax
+  | `(macro_rules $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
+  | `(macro_rules [$kind] $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
+  | _                                      => throwUnsupportedSyntax
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index da451e9f0e..6578cbf3ab 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -326,7 +326,9 @@ private def introStep (n : Name) : TacticM Unit :=
   | `(tactic| intro $h:ident)  => introStep h.getId
   | `(tactic| intro _)         => introStep `_
   | `(tactic| intro $pat:term) => do
-    let stxNew ← `(tactic| intro h; match h with | $pat:term => _; clear h)
+    let m ← `(match h with | $pat:term => _)
+    let m := m.setKind ``Lean.Parser.Tactic.match
+    let stxNew ← `(tactic| intro h; $m; clear h)
     withMacroExpansion stx stxNew $ evalTactic stxNew
   | `(tactic| intro $hs:term*) => do
     let h0 := hs.get! 0
diff --git a/src/Lean/Elab/Tactic/Induction.lean b/src/Lean/Elab/Tactic/Induction.lean
index 54b5b59af5..d8038d1c0b 100644
--- a/src/Lean/Elab/Tactic/Induction.lean
+++ b/src/Lean/Elab/Tactic/Induction.lean
@@ -23,13 +23,13 @@ open Meta
   ```
 -/
 private def getAltName (alt : Syntax) : Name :=
-  getNameOfIdent' alt[0] |>.eraseMacroScopes
+  getNameOfIdent' alt[1] |>.eraseMacroScopes
 private def getAltVarNames (alt : Syntax) : Array Name :=
-  alt[1].getArgs.map getNameOfIdent'
+  alt[2].getArgs.map getNameOfIdent'
 private def getAltRHS (alt : Syntax) : Syntax :=
-  alt[3]
+  alt[4]
 private def getAltDArrow (alt : Syntax) : Syntax :=
-  alt[2]
+  alt[3]
 
 -- Return true if `stx` is a term occurring in the RHS of the induction/cases tactic
 def isHoleRHS (rhs : Syntax) : Bool :=
@@ -241,7 +241,7 @@ private def generalizeVars (stx : Syntax) (targets : Array Expr) : TacticM Nat :
     pure (fvarIds.size, [mvarId'])
 
 private def getAltsOfInductionAlts (inductionAlts : Syntax) : Array Syntax :=
-  inductionAlts[2].getSepArgs
+  inductionAlts[1].getArgs
 
 private def getAltsOfOptInductionAlts (optInductionAlts : Syntax) : Array Syntax :=
   if optInductionAlts.isNone then #[] else getAltsOfInductionAlts optInductionAlts[0]
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 930c5d7fb6..9af4a1c561 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -16,10 +16,10 @@ structure AuxMatchTermState where
 
 private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : StateT AuxMatchTermState MacroM Syntax := do
   let matchAlts := matchTac[4]
-  let alts      := matchAlts[1].getArgs
-  let newAlts ← alts.mapSepElemsM fun alt => do
+  let alts      := matchAlts[0].getArgs
+  let newAlts ← alts.mapM fun alt => do
     let alt    := alt.setKind ``Parser.Term.matchAlt
-    let holeOrTacticSeq := alt[2]
+    let holeOrTacticSeq := alt[3]
     if holeOrTacticSeq.isOfKind ``Parser.Term.syntheticHole then
       pure alt
     else if holeOrTacticSeq.isOfKind ``Parser.Term.hole then
@@ -28,15 +28,15 @@ private def mkAuxiliaryMatchTermAux (parentTag : Name) (matchTac : Syntax) : Sta
       let holeName := mkIdentFrom holeOrTacticSeq tag
       let newHole ← `(?$holeName:ident)
       modify fun s => { s with nextIdx := s.nextIdx + 1}
-      pure $ alt.setArg 2 newHole
+      pure $ alt.setArg 3 newHole
     else withFreshMacroScope do
       let newHole ← `(?rhs)
       let newHoleId := newHole[1]
       let newCase ← `(tactic| case $newHoleId => $holeOrTacticSeq:tacticSeq )
       modify fun s => { s with cases := s.cases.push newCase }
-      pure $ alt.setArg 2 newHole
+      pure $ alt.setArg 3 newHole
   let result  := matchTac.setKind ``Parser.Term.«match»
-  let result  := result.setArg 4 (matchAlts.setArg 1 (mkNullNode newAlts))
+  let result  := result.setArg 4 (mkNode ``Parser.Term.matchAlts #[mkNullNode newAlts])
   pure result
 
 private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 3e51b40f29..f4bb2d0f20 100644
--- a/src/Lean/Parser/Term.lean
+++ b/src/Lean/Parser/Term.lean
@@ -112,12 +112,14 @@ def «forall» := parser!:leadPrec unicodeSymbol "∀ " "forall" >> many1 (ppSpa
 
 def matchAlt (rhsParser : Parser := termParser) : Parser :=
   nodeWithAntiquot "matchAlt" `Lean.Parser.Term.matchAlt $
-    sepBy1 termParser ", " >> darrow >> rhsParser
+    "| " >> ppIndent (sepBy1 termParser ", " >> darrow >> rhsParser)
+/--
+  Useful for syntax quotations. Note that generic patterns such as `` `(matchAltExpr| | ... => $rhs) `` should also
+  work with other `rhsParser`s (of arity 1). -/
+def matchAltExpr := matchAlt
 
-def matchAlts (rhsParser : Parser := termParser) (optionalFirstBar := true) : Parser :=
-  parser! ppDedent $ withPosition $
-    ppLine >> (if optionalFirstBar then optional "| " else group "| ") >>
-    sepBy1 (ppIndent <| matchAlt rhsParser) "|" (ppLine >> checkColGe "alternatives must be indented" >> "| ")
+def matchAlts (rhsParser : Parser := termParser) : Parser :=
+  parser! ppDedent $ withPosition $ many1Indent (ppLine >> matchAlt rhsParser)
 
 def matchDiscr := parser! optional (atomic (ident >> checkNoWsBefore "no space before ':'" >> ":")) >> termParser
 
@@ -129,7 +131,7 @@ def funSimpleBinder   := atomic (lookahead (many1 binderIdent >> " : ")) >> simp
 def funBinder : Parser := funImplicitBinder <|> instBinder <|> funSimpleBinder <|> termParser maxPrec
 -- NOTE: we use `nodeWithAntiquot` to ensure that `fun $b => ...` remains a `term` antiquotation
 def basicFun : Parser := nodeWithAntiquot "basicFun" `Lean.Parser.Term.basicFun (many1 (ppSpace >> funBinder) >> darrow >> termParser)
-@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts (optionalFirstBar := false))
+@[builtinTermParser] def «fun» := parser!:maxPrec unicodeSymbol "λ" "fun" >> (basicFun <|> matchAlts)
 
 def optExprPrecedence := optional (atomic ":" >> termParser maxPrec)
 @[builtinTermParser] def «parser!»  := parser!:leadPrec "parser! " >> optExprPrecedence >> termParser
@@ -144,7 +146,7 @@ def simpleBinderWithoutType := node `Lean.Parser.Term.simpleBinder (many1 binder
 def letIdLhs    : Parser := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> (simpleBinderWithoutType <|> bracketedBinder)) >> optType
 def letIdDecl   := node `Lean.Parser.Term.letIdDecl   $ atomic (letIdLhs >> " := ") >> termParser
 def letPatDecl  := node `Lean.Parser.Term.letPatDecl  $ atomic (termParser >> pushNone >> optType >> " := ") >> termParser
-def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts (optionalFirstBar := false)
+def letEqnsDecl := node `Lean.Parser.Term.letEqnsDecl $ letIdLhs >> matchAlts
 -- Remark: we use `nodeWithAntiquot` here to make sure anonymous antiquotations (e.g., `$x`) are not `letDecl`
 def letDecl     := nodeWithAntiquot "letDecl" `Lean.Parser.Term.letDecl (notFollowedBy (nonReservedSymbol "rec") "rec" >> (letIdDecl <|> letPatDecl <|> letEqnsDecl))
 @[builtinTermParser] def «let» := parser!:leadPrec  withPosition ("let " >> letDecl) >> optSemicolon termParser
@@ -163,7 +165,7 @@ def «letrec» := parser!:leadPrec withPosition (group ("let " >> nonReservedSym
 @[runBuiltinParserAttributeHooks]
 def whereDecls := parser! "where " >> many1Indent (group (optional «attributes» >> letDecl >> optional ";"))
 @[runBuiltinParserAttributeHooks]
-def matchAltsWhereDecls := parser! matchAlts (optionalFirstBar := false) >> optional whereDecls
+def matchAltsWhereDecls := parser! matchAlts >> optional whereDecls
 
 @[builtinTermParser] def nativeRefl   := parser! "nativeRefl! " >> termParser maxPrec
 @[builtinTermParser] def nativeDecide := parser! "nativeDecide!"
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index 1e75bac785..62265e4263 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -219,9 +219,8 @@ def delabAppMatch : Delab := whenPPOption getPPNotation do
     Syntax.mkApp stx st.moreArgs
   | _,        #[] => failure
   | _,        _   =>
-    let discrs ← st.discrs.mapM fun discr => `(matchDiscr|$discr:term)
     let pats ← delabPatterns st
-    let stx ← `(match $[$discrs],* with | $[$[$pats],* => $st.rhss]|*)
+    let stx ← `(match $[$st.discrs:term],* with $[| $pats,* => $st.rhss]*)
     Syntax.mkApp stx st.moreArgs
 
 @[builtinDelab mdata]
diff --git a/tests/lean/appParserIssue.lean b/tests/lean/appParserIssue.lean
index d80c2582ac..9b0c0b9006 100644
--- a/tests/lean/appParserIssue.lean
+++ b/tests/lean/appParserIssue.lean
@@ -6,7 +6,7 @@ def f (x : Nat) (g : Nat → Nat) := g x
 #check f 1 $ fun x => x -- should work
 
 syntax "foo" term:max term:max : term
-macro_rules `(foo $x $y) => `(f $x $y)
+macro_rules | `(foo $x $y) => `(f $x $y)
 
 #check foo 1 (fun x => x) -- should work
 #check foo 1 fun x => x   -- should work
diff --git a/tests/lean/match1.lean b/tests/lean/match1.lean
index 79e72797ce..af3cacd919 100644
--- a/tests/lean/match1.lean
+++ b/tests/lean/match1.lean
@@ -134,7 +134,7 @@ match n, parity n with
   | _,      _      => none
 
 -- overapplied matcher
-#check fun x => (match x with 0 => id | x+1 => id) x
+#check fun x => (match x with | 0 => id | x+1 => id) x
 
 #check fun
   | #[1, 2]    => 2
diff --git a/tests/lean/match1.lean.expected.out b/tests/lean/match1.lean.expected.out
index 89a5352b4c..eb014efe8f 100644
--- a/tests/lean/match1.lean.expected.out
+++ b/tests/lean/match1.lean.expected.out
@@ -10,16 +10,16 @@
 4
 ---- inv
 10
-match1.lean:82:0: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
+match1.lean:82:2: error: type mismatch during dependent match-elimination at pattern variable 'w' with type
   VecPred P Vec.nil
 expected type
   VecPred P tail✝
 [false, true, true]
-match1.lean:113:0: error: dependent match elimination failed, inaccessible pattern found
+match1.lean:113:2: error: dependent match elimination failed, inaccessible pattern found
   .(j + j)
 constructor expected
 [false, true, true]
-match1.lean:124:0: error: invalid match-expression, type of pattern variable 'a' contains metavariables
+match1.lean:124:11: error: invalid match-expression, type of pattern variable 'a' contains metavariables
   ?m
 fun (x : ?m × ?m) => ?m x : ?m × ?m → ?m
 fun (x : Nat × Nat) =>