# HG changeset patch
# User boehmes
# Date 1274889152 -7200
# Node ID fed6bbf35bac56ccc8de40cb0a6d3893a211fb12
# Parent  66b0ae11a358d4cbf6abcabdb474e8dd5d0d4056
try logical and theory abstraction before full abstraction (avoids warnings of linarith)

diff -r 66b0ae11a358 -r fed6bbf35bac src/HOL/Tools/SMT/z3_proof_reconstruction.ML
--- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed May 26 15:35:17 2010 +0200
+++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed May 26 17:52:32 2010 +0200
@@ -689,11 +689,19 @@
 
 fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
   named ctxt "conj/disj/distinct" prove_conj_disj_eq,
-  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
-    NAMED ctxt' "simp" (Simplifier.simp_tac simpset)
+  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
+    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
+    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
+  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
+    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
     THEN_ALL_NEW (
-      NAMED ctxt' "fast" (Classical.fast_tac HOL_cs)
-      ORELSE' NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt'))))])
+      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
+      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
+  T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
+    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
+    THEN_ALL_NEW (
+      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
+      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt'))))])
 
 end