src/HOL/Tools/SMT/z3_proof_reconstruction.ML
changeset 51717 9e7d1c139569
parent 49980 34b0464d7eef
child 52230 1105b3b5aa77
     1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Tue Apr 16 17:54:14 2013 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Thu Apr 18 17:07:01 2013 +0200
     1.3 @@ -109,7 +109,7 @@
     1.4    Classical.fast_tac (put_claset HOL_cs ctxt)
     1.5  
     1.6  fun simp_fast_tac ctxt =
     1.7 -  Simplifier.simp_tac (HOL_ss addsimps [rewr_if])
     1.8 +  Simplifier.simp_tac (put_simpset HOL_ss ctxt addsimps [rewr_if])
     1.9    THEN_ALL_NEW HOL_fast_tac ctxt
    1.10  
    1.11  end
    1.12 @@ -148,8 +148,7 @@
    1.13    val remove_fun_app = mk_meta_eq @{thm SMT.fun_app_def}
    1.14  
    1.15    fun rewrite_conv _ [] = Conv.all_conv
    1.16 -    | rewrite_conv ctxt eqs = Simplifier.full_rewrite
    1.17 -        (Simplifier.context ctxt Simplifier.empty_ss addsimps eqs)
    1.18 +    | rewrite_conv ctxt eqs = Simplifier.full_rewrite (empty_simpset ctxt addsimps eqs)
    1.19  
    1.20    val prep_rules = [@{thm Let_def}, remove_trigger, remove_weight,
    1.21      remove_fun_app, Z3_Proof_Literals.rewrite_true]
    1.22 @@ -658,7 +657,7 @@
    1.23      Z3_Proof_Tools.by_tac (
    1.24        NAMED ctxt' "arith" (Arith_Data.arith_tac ctxt')
    1.25        ORELSE' NAMED ctxt' "simp+arith" (
    1.26 -        Simplifier.asm_full_simp_tac simpset
    1.27 +        Simplifier.asm_full_simp_tac (put_simpset simpset ctxt')
    1.28          THEN_ALL_NEW Arith_Data.arith_tac ctxt')))]
    1.29  
    1.30  
    1.31 @@ -718,19 +717,19 @@
    1.32      named ctxt "pull-ite" Z3_Proof_Methods.prove_ite,
    1.33      Z3_Proof_Tools.by_abstraction 0 (true, false) ctxt [] (fn ctxt' =>
    1.34        Z3_Proof_Tools.by_tac (
    1.35 -        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac simpset)
    1.36 +        NAMED ctxt' "simp (logic)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    1.37          THEN_ALL_NEW NAMED ctxt' "fast (logic)" (fast_tac ctxt'))),
    1.38      Z3_Proof_Tools.by_abstraction 0 (false, true) ctxt [] (fn ctxt' =>
    1.39        Z3_Proof_Tools.by_tac (
    1.40          (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
    1.41 -        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac simpset)
    1.42 +        THEN' NAMED ctxt' "simp (theory)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    1.43          THEN_ALL_NEW (
    1.44            NAMED ctxt' "fast (theory)" (HOL_fast_tac ctxt')
    1.45            ORELSE' NAMED ctxt' "arith (theory)" (Arith_Data.arith_tac ctxt')))),
    1.46      Z3_Proof_Tools.by_abstraction 0 (true, true) ctxt [] (fn ctxt' =>
    1.47        Z3_Proof_Tools.by_tac (
    1.48          (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
    1.49 -        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac simpset)
    1.50 +        THEN' NAMED ctxt' "simp (full)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    1.51          THEN_ALL_NEW (
    1.52            NAMED ctxt' "fast (full)" (HOL_fast_tac ctxt')
    1.53            ORELSE' NAMED ctxt' "arith (full)" (Arith_Data.arith_tac ctxt')))),
    1.54 @@ -739,7 +738,7 @@
    1.55        (fn ctxt' =>
    1.56          Z3_Proof_Tools.by_tac (
    1.57            (Tactic.rtac @{thm iff_allI} ORELSE' K all_tac)
    1.58 -          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac simpset)
    1.59 +          THEN' NAMED ctxt' "simp (deepen)" (Simplifier.simp_tac (put_simpset simpset ctxt'))
    1.60            THEN_ALL_NEW (
    1.61              NAMED ctxt' "fast (deepen)" (HOL_fast_tac ctxt')
    1.62              ORELSE' NAMED ctxt' "arith (deepen)" (Arith_Data.arith_tac