diff --git a/src/Lean/Meta/Tactic/Split.lean b/src/Lean/Meta/Tactic/Split.lean
index dbbb928387..46d4193af3 100644
--- a/src/Lean/Meta/Tactic/Split.lean
+++ b/src/Lean/Meta/Tactic/Split.lean
@@ -57,7 +57,7 @@ def splitMatch (mvarId : MVarId) (e : Expr) : MetaM (List MVarId) := do
   let some app ← matchMatcherApp? e | throwError "match application expected"
   let (discrFVarIds, mvarId) ← generalizeMatchDiscrs mvarId app.discrs
   trace[Meta.debug] "split [1]:\n{MessageData.ofGoal mvarId}"
-  let (reverted, mvarId) ← revert mvarId discrFVarIds
+  let (reverted, mvarId) ← revert mvarId discrFVarIds (preserveOrder := true)
   let (discrFVarIds, mvarId) ← introNP mvarId discrFVarIds.size
   let numExtra := reverted.size - discrFVarIds.size
   let discrs := discrFVarIds.map mkFVar