--- a/src/HOL/Tools/SMT/z3_replay_methods.ML Mon Sep 25 20:43:21 2017 +0200
+++ b/src/HOL/Tools/SMT/z3_replay_methods.ML Tue Sep 26 15:29:59 2017 -0300
@@ -426,8 +426,10 @@
abstract_eq abstract_prop (dest_prop t))
fun arith_rewrite_tac ctxt _ =
- TRY o Simplifier.simp_tac ctxt
- THEN_ALL_NEW (Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt)
+ let val backup_tac = Arith_Data.arith_tac ctxt ORELSE' Clasimp.force_tac ctxt in
+ (TRY o Simplifier.simp_tac ctxt) THEN_ALL_NEW backup_tac
+ ORELSE' backup_tac
+ end
fun prove_arith_rewrite ctxt t =
prove_abstract' ctxt t arith_rewrite_tac (