From 84f2039b4b5161d752a757f7dbff0874ca65aebd Mon Sep 17 00:00:00 2001
From: someplaceguy <someplaceguy@wizy.org>
Date: Sat, 23 Mar 2024 19:58:36 +0000
Subject: [PATCH] HolSmt: remove workaround for #1203

Now that all known issues were fixed wrt. ARITH_PROVE not proving
goals that COOPER_PROVE could, we can remove this workaround, thus
making proof replay faster in some cases.
---
 src/HolSmt/Z3_ProofReplay.sml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/HolSmt/Z3_ProofReplay.sml b/src/HolSmt/Z3_ProofReplay.sml
index d6e06b5fd2..6b2794e025 100644
--- a/src/HolSmt/Z3_ProofReplay.sml
+++ b/src/HolSmt/Z3_ProofReplay.sml
@@ -477,13 +477,8 @@ local
              term that contains type real is provable by integer
              arithmetic *)
           profile "arith_prove(real)" RealField.REAL_ARITH_TAC goal
-        else (
+        else
           profile "arith_prove(int)" intLib.ARITH_TAC goal
-          (* the following exception handler is a workaround for this issue:
-             https://github.com/HOL-Theorem-Prover/HOL/issues/1203 *)
-          handle Feedback.HOL_ERR _ =>
-            profile "arith_prove(cooper)" intLib.COOPER_TAC goal
-        )
       val TRY = Tactical.TRY
       val ap_tactic =
         TRY AP_TERM_TAC >> TRY arith_tactic