diff --git a/src/Init/Data/Array/Basic.lean b/src/Init/Data/Array/Basic.lean
index 7bfb6bc285..b861fee931 100644
--- a/src/Init/Data/Array/Basic.lean
+++ b/src/Init/Data/Array/Basic.lean
@@ -486,7 +486,7 @@ export Array (mkArray)
 syntax "#[" sepBy(term, ", ") "]" : term
 
 macro_rules
-  | `(#[ $elems* ]) => `(List.toArray [ $elems* ])
+  | `(#[ $elems,* ]) => `(List.toArray [ $elems,* ])
 
 namespace Array
 
diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 6d407d6497..c694d61633 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -121,16 +121,16 @@ syntax "%[" term,* "|" term "]" : term -- auxiliary notation for creating big li
 namespace Lean
 
 macro_rules
-  | `([ $elems* ]) => do
+  | `([ $elems,* ]) => do
     let rec expandListLit (i : Nat) (skip : Bool) (result : Syntax) : MacroM Syntax := do
       match i, skip with
       | 0,   _     => pure result
       | i+1, true  => expandListLit i false result
-      | i+1, false => expandListLit i true  (← `(List.cons $(elems[i]) $result))
-    if elems.size < 64 then
-      expandListLit elems.size false (← `(List.nil))
+      | i+1, false => expandListLit i true  (← `(List.cons $(elems.elemsAndSeps[i]) $result))
+    if elems.elemsAndSeps.size < 64 then
+      expandListLit elems.elemsAndSeps.size false (← `(List.nil))
     else
-      `(%[ $elems* | List.nil ])
+      `(%[ $elems,* | List.nil ])
 
 namespace Parser.Tactic
 
diff --git a/src/Lean/Elab/App.lean b/src/Lean/Elab/App.lean
index 3fa54a4fe5..364d21cc47 100644
--- a/src/Lean/Elab/App.lean
+++ b/src/Lean/Elab/App.lean
@@ -384,7 +384,8 @@ private def processExplictArg (k : M Expr) : M Expr := do
       match evalSyntaxConstant env opts tacticDecl with
       | Except.error err       => throwError err
       | Except.ok tacticSyntax =>
-        let tacticBlock ← `(by { $(tacticSyntax.getArgs)* })
+        -- TODO(Leo): does this work correctly for tactic sequences?
+        let tacticBlock ← `(by $tacticSyntax)
         -- tacticBlock does not have any position information.
         -- So, we use the current ref
         let ref ← getRef
@@ -800,12 +801,12 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
     throwError "unexpected occurrence of named pattern"
   | `($id:ident) => do
     elabAppFnId id [] lvals namedArgs args expectedType? explicit ellipsis overloaded acc
-  | `($id:ident.{$us*}) => do
-    let us ← elabExplicitUnivs us.getSepElems
+  | `($id:ident.{$us,*}) => do
+    let us ← elabExplicitUnivs us
     elabAppFnId id us lvals namedArgs args expectedType? explicit ellipsis overloaded acc
   | `(@$id:ident) =>
     elabAppFn id lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
-  | `(@$id:ident.{$us*}) =>
+  | `(@$id:ident.{$us,*}) =>
     elabAppFn (f.getArg 1) lvals namedArgs args expectedType? (explicit := true) ellipsis overloaded acc
   | `(@$t)     => throwUnsupportedSyntax -- invalid occurrence of `@`
   | `(_)       => throwError "placeholders '_' cannot be used where a function is expected"
@@ -916,11 +917,11 @@ private def elabAtom : TermElab := fun stx expectedType? =>
 
 @[builtinTermElab explicit] def elabExplicit : TermElab := fun stx expectedType? =>
   match stx with
-  | `(@$id:ident)        => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
-  | `(@$id:ident.{$us*}) => elabAtom stx expectedType?
-  | `(@($t))             => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
-  | `(@$t)               => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
-  | _                    => throwUnsupportedSyntax
+  | `(@$id:ident)         => elabAtom stx expectedType?  -- Recall that `elabApp` also has support for `@`
+  | `(@$id:ident.{$us,*}) => elabAtom stx expectedType?
+  | `(@($t))              => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
+  | `(@$t)                => elabTermWithoutImplicitLambdas t expectedType?    -- `@` is being used just to disable implicit lambdas
+  | _                     => throwUnsupportedSyntax
 
 @[builtinTermElab choice] def elabChoice : TermElab := elabAtom
 @[builtinTermElab proj] def elabProj : TermElab := elabAtom
diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean
index 2576064bc7..cd20e4e40d 100644
--- a/src/Lean/Elab/BuiltinNotation.lean
+++ b/src/Lean/Elab/BuiltinNotation.lean
@@ -14,7 +14,7 @@ open Meta
 
 @[builtinTermElab anonymousCtor] def elabAnonymousCtor : TermElab := fun stx expectedType? =>
   match stx with
-  | `(⟨$args*⟩) => do
+  | `(⟨$args,*⟩) => do
     tryPostponeIfNoneOrMVar expectedType?
     match expectedType? with
     | some expectedType =>
@@ -24,7 +24,7 @@ open Meta
         (fun ival us => do
           match ival.ctors with
           | [ctor] =>
-            let newStx ← `($(mkCIdentFrom stx ctor) $(args.getSepElems)*)
+            let newStx ← `($(mkCIdentFrom stx ctor) $(args)*)
             withMacroExpansion stx newStx $ elabTerm newStx expectedType?
           | _ => throwError! "invalid constructor ⟨...⟩, expected type must be an inductive type with only one constructor {indentExpr expectedType}")
     | none => throwError "invalid constructor ⟨...⟩, expected type must be known"
@@ -262,8 +262,8 @@ private def elabCDot (stx : Syntax) (expectedType? : Option Expr) : TermElabM Ex
     let e ← elabCDot e type
     ensureHasType type e
   | `(($e))         => elabCDot e expectedType?
-  | `(($e, $es*))   => do
-    let pairs ← liftMacroM $ mkPairs (#[e] ++ es.getEvenElems)
+  | `(($e, $es,*))  => do
+    let pairs ← liftMacroM $ mkPairs (#[e] ++ es)
     withMacroExpansion stx pairs (elabTerm pairs expectedType?)
   | _ => throwError "unexpected parentheses notation"
 
diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean
index d23e9b9ac8..8231c81573 100644
--- a/src/Lean/Elab/Syntax.lean
+++ b/src/Lean/Elab/Syntax.lean
@@ -352,7 +352,7 @@ def elabMacroRulesAux (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM
     else
       throwErrorAt! alt "invalid macro_rules alternative, unexpected syntax node kind '{k'}'"
   `(@[macro $(Lean.mkIdent k)] def myMacro : Macro :=
-     fun | $alts:matchAlt* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
+     fun | $(SepArray.mk alts):matchAlt|* | _ => throw Lean.Macro.Exception.unsupportedSyntax)
 
 def inferMacroRulesAltKind (alt : Syntax) : CommandElabM SyntaxNodeKind := do
   let lhs := alt[0]
@@ -374,13 +374,13 @@ def elabNoKindMacroRulesAux (alts : Array Syntax) : CommandElabM Syntax := do
     if altsNotK.isEmpty then
       pure defCmd
     else
-      `($defCmd:command macro_rules $altsNotK:matchAlt*)
+      `($defCmd:command macro_rules $(SepArray.mk altsNotK):matchAlt|*)
 
 @[builtinCommandElab «macro_rules»] def elabMacroRules : CommandElab :=
   adaptExpander fun stx => match stx with
-  | `(macro_rules $[|]? $alts:matchAlt*)         => elabNoKindMacroRulesAux alts
-  | `(macro_rules [$kind] $[|]? $alts:matchAlt*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts
-  | _                                            => throwUnsupportedSyntax
+  | `(macro_rules $[|]? $alts:matchAlt|*)         => elabNoKindMacroRulesAux alts.elemsAndSeps
+  | `(macro_rules [$kind] $[|]? $alts:matchAlt|*) => do elabMacroRulesAux ((← getCurrNamespace) ++ kind.getId) alts.elemsAndSeps
+  | _                                             => throwUnsupportedSyntax
 
 -- TODO: cleanup after we have support for optional syntax at `match_syntax`
 @[builtinMacro Lean.Parser.Command.mixfix] def expandMixfix : Macro := fun stx =>
@@ -478,9 +478,9 @@ private def expandNotationAux (ref : Syntax)
   let fullKind := currNamespace ++ kind
   let pat := Syntax.node fullKind patArgs
   let stxDecl ← match attrKind with
-    | AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
-    | AttributeKind.local  => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $syntaxParts* : $cat)
+    | AttributeKind.global => `(syntax $[: $prec?]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
+    | AttributeKind.scoped => `(scoped syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
+    | AttributeKind.local  => `(local syntax $[: $prec? ]? [$(mkIdentFrom ref kind):ident, $(quote prio):numLit] $[$syntaxParts]* : $cat)
   let macroDecl ← `(macro_rules | `($pat) => `($qrhs))
   match (← mkSimpleDelab vars pat qrhs |>.run) with
   | some delabDecl => mkNullNode #[stxDecl, macroDecl, delabDecl]
@@ -523,7 +523,7 @@ def expandOptPrio (stx : Syntax) : Nat :=
     stx[1].isNatLit?.getD 0
 
 def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
-  let prec := stx[1].getArgs
+  let prec := stx[1].getOptional?
   let prio := expandOptPrio stx[2]
   let head := stx[3]
   let args := stx[4].getArgs
@@ -543,12 +543,13 @@ def expandMacro (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := d
   if stx.getArgs.size == 9 then
     -- `stx` is of the form `macro $head $args* : $cat => term`
     let rhs := stx[8]
-    `(syntax $prec* [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $stxParts* : $cat
+    -- NOTE: can't use `$stxParts*` here because it would interpret as a single antiquotation with the `stx` star postfix operator
+    `(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
       macro_rules | `($pat) => $rhs)
   else
     -- `stx` is of the form `macro $head $args* : $cat => `( $body )`
     let rhsBody := stx[9]
-    `(syntax $prec* [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $stxParts* : $cat
+    `(syntax $(prec)? [$(mkIdentFrom stx kind):ident, $(quote prio):numLit] $[$stxParts]* : $cat
       macro_rules | `($pat) => `($rhsBody))
 
 @[builtinCommandElab «macro»] def elabMacro : CommandElab :=
@@ -570,7 +571,7 @@ parser! "elab " >> optPrecedence >> optPrio >> elabHead >> many elabArg >> elabT
 -/
 def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
   let ref := stx
-  let prec    := stx[1].getArgs
+  let prec    := stx[1].getOptional?
   let prio    := expandOptPrio stx[2]
   let head    := stx[3]
   let args    := stx[4].getArgs
@@ -592,7 +593,7 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
   if expectedTypeSpec.hasArgs then
     if catName == `term then
       let expId := expectedTypeSpec[1]
-      `(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
+      `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
         @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
         fun stx expectedType? => match stx with
           | `($pat) => Lean.Elab.Command.withExpectedType expectedType? fun $expId => $rhs
@@ -600,19 +601,19 @@ def expandElab (currNamespace : Name) (stx : Syntax) : CommandElabM Syntax := do
     else
       throwErrorAt! expectedTypeSpec "syntax category '{catName}' does not support expected type specification"
   else if catName == `term then
-    `(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
+    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
       @[termElab $kindId:ident] def elabFn : Lean.Elab.Term.TermElab :=
       fun stx _ => match stx with
         | `($pat) => $rhs
         | _ => throwUnsupportedSyntax)
   else if catName == `command then
-    `(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
+    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
       @[commandElab $kindId:ident] def elabFn : Lean.Elab.Command.CommandElab :=
       fun
         | `($pat) => $rhs
         | _ => throwUnsupportedSyntax)
   else if catName == `tactic then
-    `(syntax $prec* [$kindId:ident, $(quote prio):numLit] $stxParts* : $cat
+    `(syntax $(prec)? [$kindId:ident, $(quote prio):numLit] $[$stxParts]* : $cat
       @[tactic $kindId:ident] def elabFn : Lean.Elab.Tactic.Tactic :=
       fun
         | `(tactic|$pat) => $rhs
diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
index c4f8839dc5..1e75bac785 100644
--- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
+++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean
@@ -459,8 +459,8 @@ def delabTuple : Delab := whenPPOption getPPNotation do
   let a ← withAppFn $ withAppArg delab
   let b ← withAppArg delab
   match b with
-  | `(($b, $bs*)) => `(($a, $b, $bs*))
-  | _             => `(($a, $b))
+  | `(($b, $bs,*)) => `(($a, $b, $bs,*))
+  | _              => `(($a, $b))
 
 -- abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β
 @[builtinDelab app.coe]
@@ -488,15 +488,15 @@ def delabConsList : Delab := whenPPOption getPPNotation do
   guard $ (← getExpr).getAppNumArgs == 3
   let x ← withAppFn (withAppArg delab)
   match (← withAppArg delab) with
-  | `([])     => `([$x])
-  | `([$xs*]) => `([$x, $xs*])
-  | _         => failure
+  | `([])      => `([$x])
+  | `([$xs,*]) => `([$x, $xs,*])
+  | _          => failure
 
 @[builtinDelab app.List.toArray]
 def delabListToArray : Delab := whenPPOption getPPNotation do
   guard $ (← getExpr).getAppNumArgs == 2
   match (← withAppArg delab) with
-  | `([$xs*]) => `(#[$xs*])
+  | `([$xs,*]) => `(#[$xs,*])
   | _         => failure
 
 @[builtinDelab app.namedPattern]
diff --git a/tests/lean/run/CommandExtOverlap.lean b/tests/lean/run/CommandExtOverlap.lean
index 3b150a88c9..233ac89bb0 100644
--- a/tests/lean/run/CommandExtOverlap.lean
+++ b/tests/lean/run/CommandExtOverlap.lean
@@ -3,8 +3,8 @@ syntax [mycheck] "#check" sepBy(term, ",") : command
 open Lean
 
 macro_rules [mycheck]
-| `(#check $es*) =>
-  let cmds := es.getSepElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[Syntax.atom {} "#check", e]
+| `(#check $es,*) =>
+  let cmds := es.getElems.map $ fun e => Syntax.node `Lean.Parser.Command.check #[Syntax.atom {} "#check", e]
   pure $ mkNullNode cmds
 
 #check true
diff --git a/tests/lean/run/macro3.lean b/tests/lean/run/macro3.lean
index 25ac4296b2..d249305190 100644
--- a/tests/lean/run/macro3.lean
+++ b/tests/lean/run/macro3.lean
@@ -1,6 +1,6 @@
 syntax "call" term:max "(" sepBy1(term, ",") ")" : term
 
 macro_rules
-| `(call $f ($args*)) => `($f $(args.getSepElems)*)
+| `(call $f ($args,*)) => `($f $args*)
 
 #check call Nat.add (1+2, 3)
diff --git a/tests/lean/run/tacticExtOverlap.lean b/tests/lean/run/tacticExtOverlap.lean
index 279cb08e41..f0255be001 100644
--- a/tests/lean/run/tacticExtOverlap.lean
+++ b/tests/lean/run/tacticExtOverlap.lean
@@ -3,7 +3,7 @@ open Lean
 syntax [myintro] "intros" sepBy(ident, ",") : tactic
 
 macro_rules [myintro]
-| `(tactic| intros $x*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x.getSepElems]
+| `(tactic| intros $x,*) => pure $ Syntax.node `Lean.Parser.Tactic.intros #[Syntax.atom {} "intros", mkNullNode x]
 
 theorem tst1 {p q : Prop} : p → q → p :=
 by {