diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index aeddcf1206..7bff2ae1ae 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -152,9 +152,8 @@ partial def evalTactic : Syntax → TacticM Unit
 | stx => withRef stx $ withIncRecDepth $ withFreshMacroScope $ match stx with
   | Syntax.node k args =>
     if k == nullKind then
-      -- list of tactics separated by `;` => evaluate in order
-      -- Syntax quotations can return multiple ones
-      stx.forSepArgsM evalTactic
+      -- Macro writers create a sequence of tactics `t₁ ... tₙ` using `mkNullNode #[t₁, ..., tₙ]`
+      stx.getArgs.forM evalTactic
     else do
       trace `Elab.step fun _ => stx;
       env ← getEnv;
diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean
index 766b24319c..6000c94197 100644
--- a/src/Lean/Elab/Tactic/Match.lean
+++ b/src/Lean/Elab/Tactic/Match.lean
@@ -44,15 +44,12 @@ private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM
 (matchTerm, s) ← (mkAuxiliaryMatchTermAux parentTag matchTac).run {};
 pure (matchTerm, s.cases)
 
-def mkTacticSeq (ref : Syntax) (tacs : Array Syntax) : Syntax :=
-mkSepStx tacs (mkAtomFrom ref "; ")
-
 @[builtinTactic Lean.Parser.Tactic.match] def evalMatch : Tactic :=
 fun stx => do
   tag ← getMainTag;
   (matchTerm, cases) ← liftMacroM $ mkAuxiliaryMatchTerm tag stx;
   refineMatchTerm ← `(tactic| refine $matchTerm);
-  let stxNew := mkTacticSeq stx (#[refineMatchTerm] ++ cases);
+  let stxNew := mkNullNode (#[refineMatchTerm] ++ cases);
   withMacroExpansion stx stxNew $ evalTactic stxNew
 
 end Tactic