diff --git a/src/Lean/Elab/Tactic/Basic.lean b/src/Lean/Elab/Tactic/Basic.lean
index c7c96e1774..c9f50dfa58 100644
--- a/src/Lean/Elab/Tactic/Basic.lean
+++ b/src/Lean/Elab/Tactic/Basic.lean
@@ -140,14 +140,9 @@ We marked these places with a `(*)` in these methods.
 /--
   Auxiliary datastructure for capturing exceptions at `evalTactic`.
 -/
-inductive EvalTacticFailure where
-  | /-- Exceptions ≠ AbortException -/ 
-    exception (s : SavedState) (ex : Exception)
-  | /-- 
-      `abort` exceptions are used when exceptions have already been logged at the message Log.
-      Thus, we save the whole state here to make sure we don't lose them.
-    -/ 
-    abort (s : SavedState)
+structure EvalTacticFailure where
+  exception : Exception
+  state : SavedState
 
 partial def evalTactic (stx : Syntax) : TacticM Unit :=
   withRef stx <| withIncRecDepth <| withFreshMacroScope <| match stx with
@@ -167,29 +162,24 @@ partial def evalTactic (stx : Syntax) : TacticM Unit :=
     | _ => throwError m!"unexpected tactic{indentD stx}"
 where 
    throwExs (failures : Array EvalTacticFailure) : TacticM Unit := do
-     let exs := failures.filterMap fun | .abort _ => none | .exception s ex => some (s, ex)
-     if h : 0 < exs.size then
-       -- Recall that `exs[0]` is the highest priority evalFn/macro
-       exs[0].1.restore (restoreInfo := true)
-       throw exs[0].2 -- (*)
+     if let some fail := failures[0]? then
+       -- Recall that `failures[0]` is the highest priority evalFn/macro
+       fail.state.restore (restoreInfo := true)
+       throw fail.exception -- (*)
      else
-       if let some (.abort s) := failures.find? fun | .abort _ => true | _ => false then
-         s.restore (restoreInfo := true)
-         throwAbortTactic
-       else
-         throwErrorAt stx "unexpected syntax {indentD stx}" 
+       throwErrorAt stx "unexpected syntax {indentD stx}"
 
     @[inline] handleEx (s : SavedState) (failures : Array EvalTacticFailure) (ex : Exception) (k : Array EvalTacticFailure → TacticM Unit) := do
       match ex with
-      | .error .. => 
-        let failures := failures.push (.exception (← Tactic.saveState) ex)
+      | .error .. =>
+        let failures := failures.push ⟨ex, ← Tactic.saveState⟩
         s.restore (restoreInfo := true); k failures
       | .internal id _ =>
         if id == unsupportedSyntaxExceptionId then
           -- We do not store `unsupportedSyntaxExceptionId`, see throwExs
           s.restore (restoreInfo := true); k failures
         else if id == abortTacticExceptionId then
-          let failures := failures.push (.abort (← Tactic.saveState))
+          let failures := failures.push ⟨ex, ← Tactic.saveState⟩
           s.restore (restoreInfo := true); k failures
         else
           throw ex -- (*)