# HG changeset patch
# User blanchet
# Date 1506450599 10800
# Node ID 00b54799bd290958c27dcef7b511b90ed897d7ca
# Parent  a8703e8ee1d317611d3247e811c4559a04b0f2e8
strengthened reconstruction tactic

diff -r a8703e8ee1d3 -r 00b54799bd29 src/HOL/Tools/SMT/z3_replay_methods.ML
--- 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 (