1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed May 26 15:35:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Wed May 26 17:52:32 2010 +0200
     1.3 @@ -689,11 +689,19 @@
     1.4  
     1.5  fun rewrite ctxt simpset ths = Thm o with_conv ctxt ths (try_apply ctxt [] [
     1.6    named ctxt "conj/disj/distinct" prove_conj_disj_eq,
     1.7 +  T.by_abstraction (true, false) ctxt [] (fn ctxt' => T.by_tac (
     1.8 +    NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
     1.9 +    THEN_ALL_NEW NAMED ctxt' "fast (logic)" (Classical.fast_tac HOL_cs))),
    1.10 +  T.by_abstraction (false, true) ctxt [] (fn ctxt' => T.by_tac (
    1.11 +    NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    1.12 +    THEN_ALL_NEW (
    1.13 +      NAMED ctxt' "fast (theory)" (Classical.fast_tac HOL_cs)
    1.14 +      ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    1.15    T.by_abstraction (true, true) ctxt [] (fn ctxt' => T.by_tac (
    1.16 -    NAMED ctxt' "simp" (Simplifier.simp_tac simpset)
    1.17 +    NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    1.18      THEN_ALL_NEW (
    1.19 -      NAMED ctxt' "fast" (Classical.fast_tac HOL_cs)
    1.20 -      ORELSE' NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt'))))])
    1.21 +      NAMED ctxt' "fast (full)" (Classical.fast_tac HOL_cs)
    1.22 +      ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt'))))])
    1.23  
    1.24  end
    1.25