renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
authorwenzelm
Thu Jul 23 18:44:09 2009 +0200 (2009-07-23)
changeset 32149ef59550a55d3
parent 32148 253f6808dabe
child 32150 4ed2865f3a56
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
doc-src/TutorialI/Protocol/Message.thy
doc-src/TutorialI/Protocol/Public.thy
src/CCL/CCL.thy
src/CCL/Type.thy
src/FOL/cladata.ML
src/FOL/simpdata.ML
src/HOL/Auth/Message.thy
src/HOL/Auth/Public.thy
src/HOL/Auth/Shared.thy
src/HOL/Auth/Smartcard/ShoupRubin.thy
src/HOL/Auth/Smartcard/ShoupRubinBella.thy
src/HOL/Auth/Smartcard/Smartcard.thy
src/HOL/Bali/Basis.thy
src/HOL/Decision_Procs/Dense_Linear_Order.thy
src/HOL/HOL.thy
src/HOL/Hoare/Hoare.thy
src/HOL/Hoare/HoareAbort.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Library/comm_ring.ML
src/HOL/Library/reflection.ML
src/HOL/MicroJava/J/JTypeSafe.thy
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_fresh_fun.ML
src/HOL/Nominal/nominal_inductive.ML
src/HOL/Nominal/nominal_inductive2.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/SET-Protocol/MessageSET.thy
src/HOL/SET-Protocol/PublicSET.thy
src/HOL/SizeChange/sct.ML
src/HOL/TLA/Memory/MemoryImplementation.thy
src/HOL/Tools/Function/decompose.ML
src/HOL/Tools/Function/fundef_core.ML
src/HOL/Tools/Function/lexicographic_order.ML
src/HOL/Tools/Function/mutual.ML
src/HOL/Tools/Function/scnp_reconstruct.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Qelim/ferrante_rackoff.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/simpdata.ML
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Simple/NSP_Bad.thy
src/HOL/UNITY/UNITY_Main.thy
src/HOL/Word/WordArith.thy
src/HOLCF/FOCUS/Buffer.thy
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/meta_theory/Abstraction.thy
src/HOLCF/IOA/meta_theory/CompoScheds.thy
src/HOLCF/IOA/meta_theory/Sequence.thy
src/HOLCF/Lift.thy
src/HOLCF/Tools/Domain/domain_theorems.ML
src/HOLCF/Tools/fixrec.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Tools/find_theorems.ML
src/Tools/eqsubst.ML
src/ZF/IntDiv_ZF.thy
src/ZF/Tools/ind_cases.ML
src/ZF/UNITY/Constrains.thy
src/ZF/UNITY/SubstAx.thy
src/ZF/int_arith.ML
     1.1 --- a/doc-src/TutorialI/Protocol/Message.thy	Thu Jul 23 18:44:08 2009 +0200
     1.2 +++ b/doc-src/TutorialI/Protocol/Message.thy	Thu Jul 23 18:44:09 2009 +0200
     1.3 @@ -915,15 +915,15 @@
     1.4  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
     1.5  
     1.6  method_setup spy_analz = {*
     1.7 -    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *}
     1.8 +    Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *}
     1.9      "for proving the Fake case when analz is involved"
    1.10  
    1.11  method_setup atomic_spy_analz = {*
    1.12 -    Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *}
    1.13 +    Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *}
    1.14      "for debugging spy_analz"
    1.15  
    1.16  method_setup Fake_insert_simp = {*
    1.17 -    Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *}
    1.18 +    Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *}
    1.19      "for debugging spy_analz"
    1.20  
    1.21  
     2.1 --- a/doc-src/TutorialI/Protocol/Public.thy	Thu Jul 23 18:44:08 2009 +0200
     2.2 +++ b/doc-src/TutorialI/Protocol/Public.thy	Thu Jul 23 18:44:09 2009 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4  ML {*
     2.5  fun possibility_tac ctxt =
     2.6      REPEAT (*omit used_Says so that Nonces start from different traces!*)
     2.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says]))
     2.8 +    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says]))
     2.9       THEN
    2.10       REPEAT_FIRST (eq_assume_tac ORELSE' 
    2.11                     resolve_tac [refl, conjI, @{thm Nonce_supply}]));
     3.1 --- a/src/CCL/CCL.thy	Thu Jul 23 18:44:08 2009 +0200
     3.2 +++ b/src/CCL/CCL.thy	Thu Jul 23 18:44:09 2009 +0200
     3.3 @@ -257,9 +257,9 @@
     3.4                  (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end
     3.5  
     3.6  fun mk_dstnct_thms thy defs inj_rls xs =
     3.7 -          let fun mk_dstnct_thm rls s = prove_goalw thy defs s
     3.8 -                               (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1])
     3.9 -          in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    3.10 +  let fun mk_dstnct_thm rls s = prove_goalw thy defs s
    3.11 +    (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1])
    3.12 +  in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end
    3.13  
    3.14  fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss)
    3.15  
     4.1 --- a/src/CCL/Type.thy	Thu Jul 23 18:44:08 2009 +0200
     4.2 +++ b/src/CCL/Type.thy	Thu Jul 23 18:44:09 2009 +0200
     4.3 @@ -132,10 +132,10 @@
     4.4    fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s
     4.5      (fn major::prems => [(resolve_tac ([major] RL top_crls) 1),
     4.6                           (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))),
     4.7 -                         (ALLGOALS (asm_simp_tac (local_simpset_of ctxt))),
     4.8 +                         (ALLGOALS (asm_simp_tac (simpset_of ctxt))),
     4.9                           (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE'
    4.10                                      etac bspec )),
    4.11 -                         (safe_tac (local_claset_of ctxt addSIs prems))])
    4.12 +                         (safe_tac (claset_of ctxt addSIs prems))])
    4.13  end
    4.14  *}
    4.15  
    4.16 @@ -408,7 +408,7 @@
    4.17  
    4.18  fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s
    4.19        (fn prems => [rtac (genXH RS iffD2) 1,
    4.20 -                    simp_tac (simpset_of thy) 1,
    4.21 +                    simp_tac (global_simpset_of thy) 1,
    4.22                      TRY (fast_tac (@{claset} addIs
    4.23                              ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI]
    4.24                               @ prems)) 1)])
    4.25 @@ -442,7 +442,7 @@
    4.26     "[| <h,h'> : lfp(%x. POgen(x) Un R Un PO);  <t,t'> : lfp(%x. POgen(x) Un R Un PO) |] ==> <h$t,h'$t'> : POgen(lfp(%x. POgen(x) Un R Un PO))"];
    4.27  
    4.28  fun POgen_tac ctxt (rla,rlb) i =
    4.29 -  SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN
    4.30 +  SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN
    4.31    rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN
    4.32    (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @
    4.33      (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i));
    4.34 @@ -481,9 +481,9 @@
    4.35  
    4.36  fun EQgen_tac ctxt rews i =
    4.37   SELECT_GOAL
    4.38 -   (TRY (safe_tac (local_claset_of ctxt)) THEN
    4.39 +   (TRY (safe_tac (claset_of ctxt)) THEN
    4.40      resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN
    4.41 -    ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN
    4.42 +    ALLGOALS (simp_tac (simpset_of ctxt)) THEN
    4.43      ALLGOALS EQgen_raw_tac) i
    4.44  *}
    4.45  
     5.1 --- a/src/FOL/cladata.ML	Thu Jul 23 18:44:08 2009 +0200
     5.2 +++ b/src/FOL/cladata.ML	Thu Jul 23 18:44:09 2009 +0200
     5.3 @@ -19,7 +19,7 @@
     5.4  structure Cla = ClassicalFun(Classical_Data);
     5.5  structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical;
     5.6  
     5.7 -ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())");
     5.8 +ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())");
     5.9  
    5.10  
    5.11  (*Propositional rules*)
     6.1 --- a/src/FOL/simpdata.ML	Thu Jul 23 18:44:08 2009 +0200
     6.2 +++ b/src/FOL/simpdata.ML	Thu Jul 23 18:44:09 2009 +0200
     6.3 @@ -164,6 +164,6 @@
     6.4  open Clasimp;
     6.5  
     6.6  ML_Antiquote.value "clasimpset"
     6.7 -  (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
     6.8 +  (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
     6.9  
    6.10  val FOL_css = (FOL_cs, FOL_ss);
     7.1 --- a/src/HOL/Auth/Message.thy	Thu Jul 23 18:44:08 2009 +0200
     7.2 +++ b/src/HOL/Auth/Message.thy	Thu Jul 23 18:44:09 2009 +0200
     7.3 @@ -939,15 +939,15 @@
     7.4  lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD]
     7.5  
     7.6  method_setup spy_analz = {*
     7.7 -    Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *}
     7.8 +    Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o clasimpset_of) *}
     7.9      "for proving the Fake case when analz is involved"
    7.10  
    7.11  method_setup atomic_spy_analz = {*
    7.12 -    Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *}
    7.13 +    Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o clasimpset_of) *}
    7.14      "for debugging spy_analz"
    7.15  
    7.16  method_setup Fake_insert_simp = {*
    7.17 -    Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *}
    7.18 +    Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o simpset_of) *}
    7.19      "for debugging spy_analz"
    7.20  
    7.21  end
     8.1 --- a/src/HOL/Auth/Public.thy	Thu Jul 23 18:44:08 2009 +0200
     8.2 +++ b/src/HOL/Auth/Public.thy	Thu Jul 23 18:44:09 2009 +0200
     8.3 @@ -407,7 +407,7 @@
     8.4  (*Tactic for possibility theorems*)
     8.5  fun possibility_tac ctxt =
     8.6      REPEAT (*omit used_Says so that Nonces start from different traces!*)
     8.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}]))
     8.8 +    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}]))
     8.9       THEN
    8.10       REPEAT_FIRST (eq_assume_tac ORELSE' 
    8.11                     resolve_tac [refl, conjI, @{thm Nonce_supply}]))
    8.12 @@ -416,7 +416,7 @@
    8.13    nonces and keys initially*)
    8.14  fun basic_possibility_tac ctxt =
    8.15      REPEAT 
    8.16 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    8.17 +    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
    8.18       THEN
    8.19       REPEAT_FIRST (resolve_tac [refl, conjI]))
    8.20  
     9.1 --- a/src/HOL/Auth/Shared.thy	Thu Jul 23 18:44:08 2009 +0200
     9.2 +++ b/src/HOL/Auth/Shared.thy	Thu Jul 23 18:44:09 2009 +0200
     9.3 @@ -204,7 +204,7 @@
     9.4      such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
     9.5  fun possibility_tac ctxt =
     9.6     (REPEAT 
     9.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt
     9.8 +    (ALLGOALS (simp_tac (simpset_of ctxt
     9.9            delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] 
    9.10            setSolver safe_solver))
    9.11       THEN
    9.12 @@ -215,7 +215,7 @@
    9.13    nonces and keys initially*)
    9.14  fun basic_possibility_tac ctxt =
    9.15      REPEAT 
    9.16 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
    9.17 +    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
    9.18       THEN
    9.19       REPEAT_FIRST (resolve_tac [refl, conjI]))
    9.20  
    10.1 --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Jul 23 18:44:08 2009 +0200
    10.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy	Thu Jul 23 18:44:09 2009 +0200
    10.3 @@ -757,7 +757,7 @@
    10.4   (*SR9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
    10.5   (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
    10.6   (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
    10.7 - (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
    10.8 + (*Base*)  (force_tac (clasimpset_of ctxt)) 1
    10.9  
   10.10  val analz_prepare_tac = 
   10.11           prepare_tac THEN
    11.1 --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Jul 23 18:44:08 2009 +0200
    11.2 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy	Thu Jul 23 18:44:09 2009 +0200
    11.3 @@ -755,7 +755,7 @@
    11.4  
    11.5  fun prepare_tac ctxt = 
    11.6   (*SR_U8*)   forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN
    11.7 - (*SR_U8*)   clarify_tac (local_claset_of ctxt) 15 THEN
    11.8 + (*SR_U8*)   clarify_tac (claset_of ctxt) 15 THEN
    11.9   (*SR_U9*)   forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN 
   11.10   (*SR_U11*)  forward_tac [@{thm Outpts_A_Card_form_10}] 21 
   11.11  
   11.12 @@ -765,7 +765,7 @@
   11.13   (*SR_U9*)   dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN 
   11.14   (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25    THEN               
   11.15   (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN                
   11.16 - (*Base*)  (force_tac (local_clasimpset_of ctxt)) 1
   11.17 + (*Base*)  (force_tac (clasimpset_of ctxt)) 1
   11.18  
   11.19  fun analz_prepare_tac ctxt = 
   11.20           prepare_tac ctxt THEN
    12.1 --- a/src/HOL/Auth/Smartcard/Smartcard.thy	Thu Jul 23 18:44:08 2009 +0200
    12.2 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy	Thu Jul 23 18:44:09 2009 +0200
    12.3 @@ -375,7 +375,7 @@
    12.4      such as  Nonce ?N \<notin> used evs that match Nonce_supply*)
    12.5  fun possibility_tac ctxt =
    12.6     (REPEAT 
    12.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt
    12.8 +    (ALLGOALS (simp_tac (simpset_of ctxt
    12.9        delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets},
   12.10          @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] 
   12.11        setSolver safe_solver))
   12.12 @@ -387,7 +387,7 @@
   12.13    nonces and keys initially*)
   12.14  fun basic_possibility_tac ctxt =
   12.15      REPEAT 
   12.16 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
   12.17 +    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
   12.18       THEN
   12.19       REPEAT_FIRST (resolve_tac [refl, conjI]))
   12.20  
    13.1 --- a/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:08 2009 +0200
    13.2 +++ b/src/HOL/Bali/Basis.thy	Thu Jul 23 18:44:09 2009 +0200
    13.3 @@ -229,7 +229,7 @@
    13.4  
    13.5  ML {*
    13.6  fun sum3_instantiate ctxt thm = map (fn s =>
    13.7 -  simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}])
    13.8 +  simplify (simpset_of ctxt delsimps[@{thm not_None_eq}])
    13.9      (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"]
   13.10  *}
   13.11  (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *)
    14.1 --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jul 23 18:44:08 2009 +0200
    14.2 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy	Thu Jul 23 18:44:09 2009 +0200
    14.3 @@ -692,7 +692,7 @@
    14.4          val clt = Thm.dest_fun2 ct
    14.5          val cz = Thm.dest_arg ct
    14.6          val neg = cr </ Rat.zero
    14.7 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
    14.8 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
    14.9                 (Thm.capply @{cterm "Trueprop"}
   14.10                    (if neg then Thm.capply (Thm.capply clt c) cz
   14.11                      else Thm.capply (Thm.capply clt cz) c))
   14.12 @@ -715,7 +715,7 @@
   14.13          val clt = Thm.dest_fun2 ct
   14.14          val cz = Thm.dest_arg ct
   14.15          val neg = cr </ Rat.zero
   14.16 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
   14.17 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
   14.18                 (Thm.capply @{cterm "Trueprop"}
   14.19                    (if neg then Thm.capply (Thm.capply clt c) cz
   14.20                      else Thm.capply (Thm.capply clt cz) c))
   14.21 @@ -736,7 +736,7 @@
   14.22          val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
   14.23          val cz = Thm.dest_arg ct
   14.24          val neg = cr </ Rat.zero
   14.25 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
   14.26 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
   14.27                 (Thm.capply @{cterm "Trueprop"}
   14.28                    (if neg then Thm.capply (Thm.capply clt c) cz
   14.29                      else Thm.capply (Thm.capply clt cz) c))
   14.30 @@ -760,7 +760,7 @@
   14.31          val clt = Drule.cterm_rule (instantiate' [SOME T] []) @{cpat "op <"}
   14.32          val cz = Thm.dest_arg ct
   14.33          val neg = cr </ Rat.zero
   14.34 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
   14.35 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
   14.36                 (Thm.capply @{cterm "Trueprop"}
   14.37                    (if neg then Thm.capply (Thm.capply clt c) cz
   14.38                      else Thm.capply (Thm.capply clt cz) c))
   14.39 @@ -779,7 +779,7 @@
   14.40          val cr = dest_frac c
   14.41          val ceq = Thm.dest_fun2 ct
   14.42          val cz = Thm.dest_arg ct
   14.43 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
   14.44 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
   14.45              (Thm.capply @{cterm "Trueprop"}
   14.46               (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
   14.47          val cth = equal_elim (symmetric cthp) TrueI
   14.48 @@ -801,7 +801,7 @@
   14.49          val cr = dest_frac c
   14.50          val ceq = Thm.dest_fun2 ct
   14.51          val cz = Thm.dest_arg ct
   14.52 -        val cthp = Simplifier.rewrite (local_simpset_of ctxt)
   14.53 +        val cthp = Simplifier.rewrite (simpset_of ctxt)
   14.54              (Thm.capply @{cterm "Trueprop"}
   14.55               (Thm.capply @{cterm "Not"} (Thm.capply (Thm.capply ceq c) cz)))
   14.56          val cth = equal_elim (symmetric cthp) TrueI
    15.1 --- a/src/HOL/HOL.thy	Thu Jul 23 18:44:08 2009 +0200
    15.2 +++ b/src/HOL/HOL.thy	Thu Jul 23 18:44:09 2009 +0200
    15.3 @@ -833,7 +833,7 @@
    15.4  open BasicClassical;
    15.5  
    15.6  ML_Antiquote.value "claset"
    15.7 -  (Scan.succeed "Classical.local_claset_of (ML_Context.the_local_context ())");
    15.8 +  (Scan.succeed "Classical.claset_of (ML_Context.the_local_context ())");
    15.9  
   15.10  structure ResAtpset = Named_Thms
   15.11    (val name = "atp" val description = "ATP rules");
    16.1 --- a/src/HOL/Hoare/Hoare.thy	Thu Jul 23 18:44:08 2009 +0200
    16.2 +++ b/src/HOL/Hoare/Hoare.thy	Thu Jul 23 18:44:09 2009 +0200
    16.3 @@ -239,7 +239,7 @@
    16.4  
    16.5  method_setup vcg_simp = {*
    16.6    Scan.succeed (fn ctxt =>
    16.7 -    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
    16.8 +    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
    16.9    "verification condition generator plus simplification"
   16.10  
   16.11  end
    17.1 --- a/src/HOL/Hoare/HoareAbort.thy	Thu Jul 23 18:44:08 2009 +0200
    17.2 +++ b/src/HOL/Hoare/HoareAbort.thy	Thu Jul 23 18:44:09 2009 +0200
    17.3 @@ -251,7 +251,7 @@
    17.4  
    17.5  method_setup vcg_simp = {*
    17.6    Scan.succeed (fn ctxt =>
    17.7 -    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *}
    17.8 +    SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *}
    17.9    "verification condition generator plus simplification"
   17.10  
   17.11  (* Special syntax for guarded statements and guarded array updates: *)
    18.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jul 23 18:44:08 2009 +0200
    18.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jul 23 18:44:09 2009 +0200
    18.3 @@ -73,7 +73,7 @@
    18.4      val MsetT = fastype_of big_Collect;
    18.5      fun Mset_incl t = mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t);
    18.6      val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect);
    18.7 -    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (local_claset_of ctxt) 1);
    18.8 +    val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1);
    18.9   in (vars, th) end;
   18.10  
   18.11  end;
    19.1 --- a/src/HOL/Library/comm_ring.ML	Thu Jul 23 18:44:08 2009 +0200
    19.2 +++ b/src/HOL/Library/comm_ring.ML	Thu Jul 23 18:44:09 2009 +0200
    19.3 @@ -89,7 +89,7 @@
    19.4  fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) =>
    19.5    let
    19.6      val thy = ProofContext.theory_of ctxt;
    19.7 -    val cring_ss = Simplifier.local_simpset_of ctxt  (*FIXME really the full simpset!?*)
    19.8 +    val cring_ss = Simplifier.simpset_of ctxt  (*FIXME really the full simpset!?*)
    19.9        addsimps cring_simps;
   19.10      val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g)
   19.11      val norm_eq_th =
    20.1 --- a/src/HOL/Library/reflection.ML	Thu Jul 23 18:44:08 2009 +0200
    20.2 +++ b/src/HOL/Library/reflection.ML	Thu Jul 23 18:44:09 2009 +0200
    20.3 @@ -285,7 +285,7 @@
    20.4      val th' = instantiate ([], cvs) th
    20.5      val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th'
    20.6      val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t')))
    20.7 -	       (fn _ => simp_tac (local_simpset_of ctxt) 1)
    20.8 +	       (fn _ => simp_tac (simpset_of ctxt) 1)
    20.9    in FWD trans [th'',th']
   20.10    end
   20.11  
    21.1 --- a/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Jul 23 18:44:08 2009 +0200
    21.2 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy	Thu Jul 23 18:44:09 2009 +0200
    21.3 @@ -204,7 +204,7 @@
    21.4  apply( simp_all)
    21.5  apply( tactic "ALLGOALS strip_tac")
    21.6  apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"]
    21.7 -                 THEN_ALL_NEW (full_simp_tac (simpset_of @{theory Conform}))) *})
    21.8 +                 THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *})
    21.9  apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])")
   21.10  
   21.11  -- "Level 7"
    22.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Jul 23 18:44:08 2009 +0200
    22.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Jul 23 18:44:09 2009 +0200
    22.3 @@ -109,7 +109,7 @@
    22.4  (
    22.5  OldGoals.push_proof();
    22.6  OldGoals.goalw_cterm [] (cterm_of sign trm);
    22.7 -by (simp_tac (simpset_of sign) 1);
    22.8 +by (simp_tac (global_simpset_of sign) 1);
    22.9          let
   22.10          val if_tmp_result = result()
   22.11          in
    23.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 23 18:44:08 2009 +0200
    23.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jul 23 18:44:09 2009 +0200
    23.3 @@ -324,7 +324,7 @@
    23.4               (perm_names_types ~~ perm_indnames))))
    23.5            (fn _ => EVERY [indtac induction perm_indnames 1,
    23.6              ALLGOALS (asm_full_simp_tac
    23.7 -              (simpset_of thy2 addsimps [perm_fun_def]))])),
    23.8 +              (global_simpset_of thy2 addsimps [perm_fun_def]))])),
    23.9          length new_type_names));
   23.10  
   23.11      (**** prove [] \<bullet> t = t ****)
   23.12 @@ -344,7 +344,7 @@
   23.13                 (perm_names ~~
   23.14                  map body_type perm_types ~~ perm_indnames)))))
   23.15            (fn _ => EVERY [indtac induction perm_indnames 1,
   23.16 -            ALLGOALS (asm_full_simp_tac (simpset_of thy2))])),
   23.17 +            ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])),
   23.18          length new_type_names))
   23.19        end)
   23.20        atoms);
   23.21 @@ -379,7 +379,7 @@
   23.22                    (perm_names ~~
   23.23                     map body_type perm_types ~~ perm_indnames)))))
   23.24             (fn _ => EVERY [indtac induction perm_indnames 1,
   23.25 -              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
   23.26 +              ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))),
   23.27           length new_type_names)
   23.28        end) atoms);
   23.29  
   23.30 @@ -415,7 +415,7 @@
   23.31                    (perm_names ~~
   23.32                     map body_type perm_types ~~ perm_indnames))))))
   23.33             (fn _ => EVERY [indtac induction perm_indnames 1,
   23.34 -              ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
   23.35 +              ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))),
   23.36           length new_type_names)
   23.37        end) atoms);
   23.38  
   23.39 @@ -437,7 +437,7 @@
   23.40          val permT2 = mk_permT (Type (name2, []));
   23.41          val Ts = map body_type perm_types;
   23.42          val cp_inst = cp_inst_of thy name1 name2;
   23.43 -        val simps = simpset_of thy addsimps (perm_fun_def ::
   23.44 +        val simps = global_simpset_of thy addsimps (perm_fun_def ::
   23.45            (if name1 <> name2 then
   23.46               let val dj = dj_thm_of thy name2 name1
   23.47               in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end
   23.48 @@ -601,7 +601,7 @@
   23.49                 end) (rep_set_names'' ~~ recTs' ~~ perm_indnames')))))
   23.50          (fn _ => EVERY
   23.51             [indtac rep_induct [] 1,
   23.52 -            ALLGOALS (simp_tac (simpset_of thy4 addsimps
   23.53 +            ALLGOALS (simp_tac (global_simpset_of thy4 addsimps
   23.54                (symmetric perm_fun_def :: abs_perm))),
   23.55              ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])),
   23.56          length new_type_names));
   23.57 @@ -661,8 +661,8 @@
   23.58                map (inter_sort thy sort o snd) tvs, [pt_class])
   23.59              (EVERY [Class.intro_classes_tac [],
   23.60                rewrite_goals_tac [perm_def],
   23.61 -              asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1,
   23.62 -              asm_full_simp_tac (simpset_of thy addsimps
   23.63 +              asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1,
   23.64 +              asm_full_simp_tac (global_simpset_of thy addsimps
   23.65                  [Rep RS perm_closed RS Abs_inverse]) 1,
   23.66                asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy
   23.67                  ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy
   23.68 @@ -690,7 +690,7 @@
   23.69                map (inter_sort thy sort o snd) tvs, [cp_class])
   23.70              (EVERY [Class.intro_classes_tac [],
   23.71                rewrite_goals_tac [perm_def],
   23.72 -              asm_full_simp_tac (simpset_of thy addsimps
   23.73 +              asm_full_simp_tac (global_simpset_of thy addsimps
   23.74                  ((Rep RS perm_closed1 RS Abs_inverse) ::
   23.75                   (if atom1 = atom2 then []
   23.76                    else [Rep RS perm_closed2 RS Abs_inverse]))) 1,
   23.77 @@ -875,7 +875,7 @@
   23.78        | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) =
   23.79            let
   23.80              val dist_thm = Goal.prove_global thy8 [] [] t (fn _ =>
   23.81 -              simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   23.82 +              simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1)
   23.83            in dist_thm :: standard (dist_thm RS not_sym) ::
   23.84              prove_distinct_thms p (k, ts)
   23.85            end;
   23.86 @@ -920,7 +920,7 @@
   23.87                (HOLogic.mk_Trueprop (HOLogic.mk_eq
   23.88                  (perm (list_comb (c, l_args)), list_comb (c, r_args)))))
   23.89              (fn _ => EVERY
   23.90 -              [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
   23.91 +              [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1,
   23.92                 simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @
   23.93                   constr_defs @ perm_closed_thms)) 1,
   23.94                 TRY (simp_tac (HOL_basic_ss addsimps
   23.95 @@ -973,7 +973,7 @@
   23.96                  (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)),
   23.97                   foldr1 HOLogic.mk_conj eqs))))
   23.98              (fn _ => EVERY
   23.99 -               [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm ::
  23.100 +               [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm ::
  23.101                    rep_inject_thms')) 1,
  23.102                  TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def ::
  23.103                    alpha @ abs_perm @ abs_fresh @ rep_inject_thms @
  23.104 @@ -1100,7 +1100,7 @@
  23.105                     (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T)))
  23.106                     (indnames ~~ recTs)))))
  23.107             (fn _ => indtac dt_induct indnames 1 THEN
  23.108 -            ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps
  23.109 +            ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps
  23.110                (abs_supp @ supp_atm @
  23.111                 PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @
  23.112                 List.concat supp_thms))))),
    24.1 --- a/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jul 23 18:44:08 2009 +0200
    24.2 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML	Thu Jul 23 18:44:09 2009 +0200
    24.3 @@ -143,7 +143,7 @@
    24.4    let
    24.5      val thy = theory_of_thm thm;
    24.6      val ctx = Context.init_proof thy;
    24.7 -    val ss = simpset_of thy;
    24.8 +    val ss = global_simpset_of thy;
    24.9      val abs_fresh = PureThy.get_thms thy "abs_fresh";
   24.10      val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app";
   24.11      val ss' = ss addsimps fresh_prod::abs_fresh;
    25.1 --- a/src/HOL/Nominal/nominal_inductive.ML	Thu Jul 23 18:44:08 2009 +0200
    25.2 +++ b/src/HOL/Nominal/nominal_inductive.ML	Thu Jul 23 18:44:09 2009 +0200
    25.3 @@ -403,7 +403,7 @@
    25.4            cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
    25.5            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
    25.6              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
    25.7 -            asm_full_simp_tac (simpset_of thy) 1)
    25.8 +            asm_full_simp_tac (simpset_of ctxt) 1)
    25.9          end) |> singleton (ProofContext.export ctxt' ctxt);
   25.10  
   25.11      (** strong case analysis rule **)
    26.1 --- a/src/HOL/Nominal/nominal_inductive2.ML	Thu Jul 23 18:44:08 2009 +0200
    26.2 +++ b/src/HOL/Nominal/nominal_inductive2.ML	Thu Jul 23 18:44:09 2009 +0200
    26.3 @@ -438,7 +438,7 @@
    26.4            cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN
    26.5            REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN
    26.6              etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN
    26.7 -            asm_full_simp_tac (simpset_of thy) 1)
    26.8 +            asm_full_simp_tac (simpset_of ctxt) 1)
    26.9          end) |>
   26.10          fresh_postprocess |>
   26.11          singleton (ProofContext.export ctxt' ctxt);
    27.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Jul 23 18:44:08 2009 +0200
    27.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Jul 23 18:44:09 2009 +0200
    27.3 @@ -404,19 +404,19 @@
    27.4    Method.sections (Simplifier.simp_modifiers') >>
    27.5    (fn (prems, tac) => fn ctxt => METHOD (fn facts =>
    27.6      HEADGOAL (Method.insert_tac (prems @ facts) THEN'
    27.7 -      (CHANGED_PROP oo tac) (local_simpset_of ctxt))));
    27.8 +      (CHANGED_PROP oo tac) (simpset_of ctxt))));
    27.9  
   27.10  (* setup so that the simpset is used which is active at the moment when the tactic is called *)
   27.11  fun local_simp_meth_setup tac =
   27.12    Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   27.13 -  (K (SIMPLE_METHOD' o tac o local_simpset_of));
   27.14 +  (K (SIMPLE_METHOD' o tac o simpset_of));
   27.15  
   27.16  (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *)
   27.17  
   27.18  fun basic_simp_meth_setup debug tac =
   27.19    Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) --
   27.20    Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >>
   27.21 -  (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o local_simpset_of));
   27.22 +  (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o simpset_of));
   27.23  
   27.24  val perm_simp_meth_debug        = local_simp_meth_setup dperm_simp_tac;
   27.25  val perm_extend_simp_meth       = local_simp_meth_setup perm_extend_simp_tac;
    28.1 --- a/src/HOL/SET-Protocol/MessageSET.thy	Thu Jul 23 18:44:08 2009 +0200
    28.2 +++ b/src/HOL/SET-Protocol/MessageSET.thy	Thu Jul 23 18:44:09 2009 +0200
    28.3 @@ -939,17 +939,17 @@
    28.4  
    28.5  method_setup spy_analz = {*
    28.6      Scan.succeed (fn ctxt =>
    28.7 -        SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *}
    28.8 +        SIMPLE_METHOD' (MessageSET.spy_analz_tac (clasimpset_of ctxt))) *}
    28.9      "for proving the Fake case when analz is involved"
   28.10  
   28.11  method_setup atomic_spy_analz = {*
   28.12      Scan.succeed (fn ctxt =>
   28.13 -        SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *}
   28.14 +        SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (clasimpset_of ctxt))) *}
   28.15      "for debugging spy_analz"
   28.16  
   28.17  method_setup Fake_insert_simp = {*
   28.18      Scan.succeed (fn ctxt =>
   28.19 -        SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *}
   28.20 +        SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (simpset_of ctxt))) *}
   28.21      "for debugging spy_analz"
   28.22  
   28.23  end
    29.1 --- a/src/HOL/SET-Protocol/PublicSET.thy	Thu Jul 23 18:44:08 2009 +0200
    29.2 +++ b/src/HOL/SET-Protocol/PublicSET.thy	Thu Jul 23 18:44:09 2009 +0200
    29.3 @@ -350,7 +350,7 @@
    29.4  (*Tactic for possibility theorems*)
    29.5  fun possibility_tac ctxt =
    29.6      REPEAT (*omit used_Says so that Nonces start from different traces!*)
    29.7 -    (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
    29.8 +    (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}]))
    29.9       THEN
   29.10       REPEAT_FIRST (eq_assume_tac ORELSE' 
   29.11                     resolve_tac [refl, conjI, @{thm Nonce_supply}]))
   29.12 @@ -359,7 +359,7 @@
   29.13    nonces and keys initially*)
   29.14  fun basic_possibility_tac ctxt =
   29.15      REPEAT 
   29.16 -    (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver))
   29.17 +    (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver))
   29.18       THEN
   29.19       REPEAT_FIRST (resolve_tac [refl, conjI]))
   29.20  
    30.1 --- a/src/HOL/SizeChange/sct.ML	Thu Jul 23 18:44:08 2009 +0200
    30.2 +++ b/src/HOL/SizeChange/sct.ML	Thu Jul 23 18:44:09 2009 +0200
    30.3 @@ -184,7 +184,7 @@
    30.4  
    30.5  fun setup_probe_goal ctxt domT Dtab Mtab (i, j) =
    30.6      let
    30.7 -      val css = local_clasimpset_of ctxt
    30.8 +      val css = clasimpset_of ctxt
    30.9        val thy = ProofContext.theory_of ctxt
   30.10        val RD1 = get_elem (Dtab i)
   30.11        val RD2 = get_elem (Dtab j)
   30.12 @@ -269,7 +269,7 @@
   30.13  
   30.14  fun in_graph_tac ctxt =
   30.15      simp_tac (HOL_basic_ss addsimps has_edge_simps) 1
   30.16 -    THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *)
   30.17 +    THEN (simp_tac (simpset_of ctxt) 1) (* FIXME reduce simpset *)
   30.18  
   30.19  fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1
   30.20    | approx_tac ctxt (Graph (G, thm)) =
   30.21 @@ -334,7 +334,7 @@
   30.22        val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns)
   30.23  
   30.24        val tac =
   30.25 -          unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt)
   30.26 +          unfold_tac [sound_int_def, len_simp] (simpset_of ctxt)
   30.27              THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts)
   30.28      in
   30.29        tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st)
    31.1 --- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Jul 23 18:44:08 2009 +0200
    31.2 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Thu Jul 23 18:44:09 2009 +0200
    31.3 @@ -763,7 +763,7 @@
    31.4  *)
    31.5  ML {*
    31.6  fun split_idle_tac ctxt simps i =
    31.7 -  let val ss = Simplifier.local_simpset_of ctxt in
    31.8 +  let val ss = simpset_of ctxt in
    31.9      TRY (rtac @{thm actionI} i) THEN
   31.10      InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN
   31.11      rewrite_goals_tac @{thms action_rews} THEN
    32.1 --- a/src/HOL/Tools/Function/decompose.ML	Thu Jul 23 18:44:08 2009 +0200
    32.2 +++ b/src/HOL/Tools/Function/decompose.ML	Thu Jul 23 18:44:09 2009 +0200
    32.3 @@ -98,7 +98,7 @@
    32.4  
    32.5  fun auto_decompose_tac ctxt =
    32.6      Termination.TERMINATION ctxt
    32.7 -      (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt))
    32.8 +      (decompose_tac ctxt (auto_tac (clasimpset_of ctxt))
    32.9                       (K (K all_tac)) (K (K no_tac)))
   32.10  
   32.11  
    33.1 --- a/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 23 18:44:08 2009 +0200
    33.2 +++ b/src/HOL/Tools/Function/fundef_core.ML	Thu Jul 23 18:44:09 2009 +0200
    33.3 @@ -702,7 +702,7 @@
    33.4        Goal.init goal
    33.5        |> (SINGLE (resolve_tac [accI] 1)) |> the
    33.6        |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1))  |> the
    33.7 -      |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the
    33.8 +      |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the
    33.9        |> Goal.conclude
   33.10        |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   33.11      end
   33.12 @@ -831,7 +831,7 @@
   33.13                           ((rtac (G_induct OF [a]))
   33.14                              THEN_ALL_NEW (rtac accI)
   33.15                              THEN_ALL_NEW (etac R_cases)
   33.16 -                            THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1)
   33.17 +                            THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1)
   33.18  
   33.19        val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value)
   33.20  
   33.21 @@ -849,9 +849,9 @@
   33.22                         (fn _ =>
   33.23                             rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1
   33.24                                  THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1
   33.25 -                                THEN (simp_default_tac (local_simpset_of ctxt) 1)
   33.26 +                                THEN (simp_default_tac (simpset_of ctxt) 1)
   33.27                                  THEN (etac not_acc_down 1)
   33.28 -                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1)
   33.29 +                                THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1)
   33.30                |> fold_rev forall_intr_rename (map fst oqs ~~ cqs)
   33.31            end
   33.32      in
    34.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 18:44:08 2009 +0200
    34.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML	Thu Jul 23 18:44:09 2009 +0200
    34.3 @@ -217,7 +217,7 @@
    34.4  fun lexicographic_order_tac ctxt =
    34.5    TRY (FundefCommon.apply_termination_rule ctxt 1)
    34.6    THEN lex_order_tac ctxt
    34.7 -    (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
    34.8 +    (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt))
    34.9  
   34.10  val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac
   34.11  
    35.1 --- a/src/HOL/Tools/Function/mutual.ML	Thu Jul 23 18:44:08 2009 +0200
    35.2 +++ b/src/HOL/Tools/Function/mutual.ML	Thu Jul 23 18:44:09 2009 +0200
    35.3 @@ -206,7 +206,7 @@
    35.4                   (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs))
    35.5                   (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs)
    35.6                            THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1
    35.7 -                          THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
    35.8 +                          THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1)
    35.9          |> restore_cond 
   35.10          |> export
   35.11      end
    36.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 23 18:44:08 2009 +0200
    36.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML	Thu Jul 23 18:44:09 2009 +0200
    36.3 @@ -291,7 +291,7 @@
    36.4           THEN (rtac @{thm rp_inv_image_rp} 1)
    36.5           THEN (rtac (order_rpair ms_rp label) 1)
    36.6           THEN PRIMITIVE (instantiate' [] [SOME level_mapping])
    36.7 -         THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt)
    36.8 +         THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt)
    36.9           THEN LocalDefs.unfold_tac ctxt
   36.10             (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv})
   36.11           THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}]))
   36.12 @@ -406,7 +406,7 @@
   36.13  fun decomp_scnp orders ctxt =
   36.14    let
   36.15      val extra_simps = FundefCommon.Termination_Simps.get ctxt
   36.16 -    val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps)
   36.17 +    val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps)
   36.18    in
   36.19      SIMPLE_METHOD
   36.20        (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt))
    37.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 23 18:44:08 2009 +0200
    37.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 23 18:44:09 2009 +0200
    37.3 @@ -303,7 +303,7 @@
    37.4            THEN' ((rtac @{thm refl})                       (* unification instantiates all Vars *)
    37.5                   ORELSE' ((rtac @{thm conjI})
    37.6                            THEN' (rtac @{thm refl})
    37.7 -                          THEN' (blast_tac (local_claset_of ctxt))))  (* Solve rest of context... not very elegant *)
    37.8 +                          THEN' (blast_tac (claset_of ctxt))))  (* Solve rest of context... not very elegant *)
    37.9            ) i
   37.10      in
   37.11        ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)])
    38.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Jul 23 18:44:08 2009 +0200
    38.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML	Thu Jul 23 18:44:09 2009 +0200
    38.3 @@ -228,6 +228,6 @@
    38.4        ObjectLogic.full_atomize_tac i THEN
    38.5        simp_tac (#simpset (snd instance)) i THEN  (* FIXME already part of raw_ferrack_qe_conv? *)
    38.6        CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN
    38.7 -      simp_tac (Simplifier.local_simpset_of ctxt) i));  (* FIXME really? *)
    38.8 +      simp_tac (simpset_of ctxt) i));  (* FIXME really? *)
    38.9  
   38.10  end;
    39.1 --- a/src/HOL/Tools/inductive.ML	Thu Jul 23 18:44:08 2009 +0200
    39.2 +++ b/src/HOL/Tools/inductive.ML	Thu Jul 23 18:44:09 2009 +0200
    39.3 @@ -425,7 +425,7 @@
    39.4  fun mk_cases ctxt prop =
    39.5    let
    39.6      val thy = ProofContext.theory_of ctxt;
    39.7 -    val ss = Simplifier.local_simpset_of ctxt;
    39.8 +    val ss = simpset_of ctxt;
    39.9  
   39.10      fun err msg =
   39.11        error (Pretty.string_of (Pretty.block
    40.1 --- a/src/HOL/Tools/recdef.ML	Thu Jul 23 18:44:08 2009 +0200
    40.2 +++ b/src/HOL/Tools/recdef.ML	Thu Jul 23 18:44:09 2009 +0200
    40.3 @@ -172,15 +172,15 @@
    40.4          NONE => ctxt0
    40.5        | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0));
    40.6      val {simps, congs, wfs} = get_hints ctxt;
    40.7 -    val cs = local_claset_of ctxt;
    40.8 -    val ss = local_simpset_of ctxt addsimps simps;
    40.9 +    val cs = claset_of ctxt;
   40.10 +    val ss = simpset_of ctxt addsimps simps;
   40.11    in (cs, ss, rev (map snd congs), wfs) end;
   40.12  
   40.13  fun prepare_hints_i thy () =
   40.14    let
   40.15      val ctxt0 = ProofContext.init thy;
   40.16      val {simps, congs, wfs} = get_global_hints thy;
   40.17 -  in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
   40.18 +  in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end;
   40.19  
   40.20  
   40.21  
    41.1 --- a/src/HOL/Tools/simpdata.ML	Thu Jul 23 18:44:08 2009 +0200
    41.2 +++ b/src/HOL/Tools/simpdata.ML	Thu Jul 23 18:44:09 2009 +0200
    41.3 @@ -158,7 +158,7 @@
    41.4  open Clasimp;
    41.5  
    41.6  val _ = ML_Antiquote.value "clasimpset"
    41.7 -  (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())");
    41.8 +  (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())");
    41.9  
   41.10  val mksimps_pairs =
   41.11    [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]),
    42.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 18:44:08 2009 +0200
    42.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 18:44:09 2009 +0200
    42.3 @@ -321,7 +321,7 @@
    42.4  *}
    42.5  
    42.6  method_setup record_auto = {*
    42.7 -  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt)))
    42.8 +  Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt)))
    42.9  *} ""
   42.10  
   42.11  lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   42.12 @@ -714,7 +714,7 @@
   42.13  
   42.14  method_setup rename_client_map = {*
   42.15    Scan.succeed (fn ctxt =>
   42.16 -    SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt)))
   42.17 +    SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt)))
   42.18  *} ""
   42.19  
   42.20  text{*Lifting @{text Client_Increasing} to @{term systemState}*}
    43.1 --- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 23 18:44:08 2009 +0200
    43.2 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Thu Jul 23 18:44:09 2009 +0200
    43.3 @@ -125,7 +125,7 @@
    43.4  
    43.5  method_setup ns_induct = {*
    43.6      Scan.succeed (fn ctxt =>
    43.7 -        SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *}
    43.8 +        SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *}
    43.9      "for inductive reasoning about the Needham-Schroeder protocol"
   43.10  
   43.11  text{*Converts invariants into statements about reachable states*}
    44.1 --- a/src/HOL/UNITY/UNITY_Main.thy	Thu Jul 23 18:44:08 2009 +0200
    44.2 +++ b/src/HOL/UNITY/UNITY_Main.thy	Thu Jul 23 18:44:09 2009 +0200
    44.3 @@ -11,12 +11,12 @@
    44.4  
    44.5  method_setup safety = {*
    44.6      Scan.succeed (fn ctxt =>
    44.7 -        SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *}
    44.8 +        SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *}
    44.9      "for proving safety properties"
   44.10  
   44.11  method_setup ensures_tac = {*
   44.12    Args.goal_spec -- Scan.lift Args.name_source >>
   44.13 -  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s))
   44.14 +  (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s))
   44.15  *} "for proving progress properties"
   44.16  
   44.17  end
    45.1 --- a/src/HOL/Word/WordArith.thy	Thu Jul 23 18:44:08 2009 +0200
    45.2 +++ b/src/HOL/Word/WordArith.thy	Thu Jul 23 18:44:09 2009 +0200
    45.3 @@ -513,8 +513,8 @@
    45.4  fun uint_arith_tacs ctxt = 
    45.5    let
    45.6      fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
    45.7 -    val cs = local_claset_of ctxt;
    45.8 -    val ss = local_simpset_of ctxt;
    45.9 +    val cs = claset_of ctxt;
   45.10 +    val ss = simpset_of ctxt;
   45.11    in 
   45.12      [ clarify_tac cs 1,
   45.13        full_simp_tac (uint_arith_ss_of ss) 1,
   45.14 @@ -1075,8 +1075,8 @@
   45.15  fun unat_arith_tacs ctxt =   
   45.16    let
   45.17      fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
   45.18 -    val cs = local_claset_of ctxt;
   45.19 -    val ss = local_simpset_of ctxt;
   45.20 +    val cs = claset_of ctxt;
   45.21 +    val ss = simpset_of ctxt;
   45.22    in 
   45.23      [ clarify_tac cs 1,
   45.24        full_simp_tac (unat_arith_ss_of ss) 1,
    46.1 --- a/src/HOLCF/FOCUS/Buffer.thy	Thu Jul 23 18:44:08 2009 +0200
    46.2 +++ b/src/HOLCF/FOCUS/Buffer.thy	Thu Jul 23 18:44:09 2009 +0200
    46.3 @@ -101,7 +101,7 @@
    46.4  fun B_prover s tac eqs =
    46.5    let val thy = the_context () in
    46.6      prove_goal thy s (fn prems => [cut_facts_tac prems 1,
    46.7 -        tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)])
    46.8 +        tac 1, auto_tac (global_claset_of thy, global_simpset_of thy addsimps eqs)])
    46.9    end;
   46.10  
   46.11  fun prove_forw  s thm     = B_prover s (dtac (thm RS iffD1)) [];
    47.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jul 23 18:44:08 2009 +0200
    47.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jul 23 18:44:09 2009 +0200
    47.3 @@ -278,14 +278,14 @@
    47.4  by (REPEAT (rtac impI 1));
    47.5  by (REPEAT (dtac eq_reflection 1));
    47.6  (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
    47.7 -by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
    47.8 +by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs)
    47.9                                delsimps [not_iff,split_part])
   47.10  			      addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
   47.11                                          rename_simps @ ioa_simps @ asig_simps)) 1);
   47.12  by (full_simp_tac
   47.13    (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1);
   47.14  by (REPEAT (if_full_simp_tac
   47.15 -  (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
   47.16 +  (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1));
   47.17  by (call_mucke_tac 1);
   47.18  (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
   47.19  by (atac 1);
    48.1 --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Jul 23 18:44:08 2009 +0200
    48.2 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy	Thu Jul 23 18:44:09 2009 +0200
    48.3 @@ -605,7 +605,7 @@
    48.4  
    48.5  ML {*
    48.6  fun abstraction_tac ctxt =
    48.7 -  let val (cs, ss) = local_clasimpset_of ctxt in
    48.8 +  let val (cs, ss) = clasimpset_of ctxt in
    48.9      SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas},
   48.10          ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
   48.11    end
    49.1 --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Jul 23 18:44:08 2009 +0200
    49.2 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy	Thu Jul 23 18:44:09 2009 +0200
    49.3 @@ -299,10 +299,10 @@
    49.4  in
    49.5  
    49.6  fun mkex_induct_tac ctxt sch exA exB =
    49.7 -  let val ss = Simplifier.local_simpset_of ctxt in
    49.8 +  let val ss = simpset_of ctxt in
    49.9      EVERY1[Seq_induct_tac ctxt sch defs,
   49.10             asm_full_simp_tac ss,
   49.11 -           SELECT_GOAL (safe_tac (claset_of @{theory Fun})),
   49.12 +           SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})),
   49.13             Seq_case_simp_tac ctxt exA,
   49.14             Seq_case_simp_tac ctxt exB,
   49.15             asm_full_simp_tac ss,
    50.1 --- a/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jul 23 18:44:08 2009 +0200
    50.2 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy	Thu Jul 23 18:44:09 2009 +0200
    50.3 @@ -1091,7 +1091,7 @@
    50.4  
    50.5  (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *)
    50.6  fun Seq_case_simp_tac ctxt s i =
    50.7 -  let val ss = Simplifier.local_simpset_of ctxt in
    50.8 +  let val ss = simpset_of ctxt in
    50.9      Seq_case_tac ctxt s i
   50.10      THEN asm_simp_tac ss (i+2)
   50.11      THEN asm_full_simp_tac ss (i+1)
   50.12 @@ -1100,7 +1100,7 @@
   50.13  
   50.14  (* rws are definitions to be unfolded for admissibility check *)
   50.15  fun Seq_induct_tac ctxt s rws i =
   50.16 -  let val ss = Simplifier.local_simpset_of ctxt in
   50.17 +  let val ss = simpset_of ctxt in
   50.18      res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   50.19      THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1))))
   50.20      THEN simp_tac (ss addsimps rws) i
   50.21 @@ -1108,15 +1108,15 @@
   50.22  
   50.23  fun Seq_Finite_induct_tac ctxt i =
   50.24    etac @{thm Seq_Finite_ind} i
   50.25 -  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i)));
   50.26 +  THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i)));
   50.27  
   50.28  fun pair_tac ctxt s =
   50.29    res_inst_tac ctxt [(("p", 0), s)] PairE
   50.30 -  THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt);
   50.31 +  THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt);
   50.32  
   50.33  (* induction on a sequence of pairs with pairsplitting and simplification *)
   50.34  fun pair_induct_tac ctxt s rws i =
   50.35 -  let val ss = Simplifier.local_simpset_of ctxt in
   50.36 +  let val ss = simpset_of ctxt in
   50.37      res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i
   50.38      THEN pair_tac ctxt "a" (i+3)
   50.39      THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1))))
    51.1 --- a/src/HOLCF/Lift.thy	Thu Jul 23 18:44:08 2009 +0200
    51.2 +++ b/src/HOLCF/Lift.thy	Thu Jul 23 18:44:09 2009 +0200
    51.3 @@ -61,7 +61,7 @@
    51.4  
    51.5  method_setup defined = {*
    51.6    Scan.succeed (fn ctxt => SIMPLE_METHOD'
    51.7 -    (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt)))
    51.8 +    (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt)))
    51.9  *} ""
   51.10  
   51.11  lemma DefE: "Def x = \<bottom> \<Longrightarrow> R"
    52.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jul 23 18:44:08 2009 +0200
    52.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jul 23 18:44:09 2009 +0200
    52.3 @@ -685,7 +685,7 @@
    52.4  (* ----- theorems concerning finite approximation and finite induction ------ *)
    52.5  
    52.6  local
    52.7 -  val iterate_Cprod_ss = simpset_of @{theory Fix};
    52.8 +  val iterate_Cprod_ss = global_simpset_of @{theory Fix};
    52.9    val copy_con_rews  = copy_rews @ con_rews;
   52.10    val copy_take_defs =
   52.11      (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def;
    53.1 --- a/src/HOLCF/Tools/fixrec.ML	Thu Jul 23 18:44:08 2009 +0200
    53.2 +++ b/src/HOLCF/Tools/fixrec.ML	Thu Jul 23 18:44:09 2009 +0200
    53.3 @@ -158,13 +158,13 @@
    53.4      val thy = ProofContext.theory_of lthy;
    53.5      val names = map (Binding.name_of o fst o fst) fixes;
    53.6      val all_names = space_implode "_" names;
    53.7 -    val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
    53.8 +    val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec);
    53.9      val functional = lambda_tuple lhss (mk_tuple rhss);
   53.10      val fixpoint = mk_fix (mk_cabs functional);
   53.11      
   53.12      val cont_thm =
   53.13        Goal.prove lthy [] [] (mk_trp (mk_cont functional))
   53.14 -        (K (simp_tac (local_simpset_of lthy) 1));
   53.15 +        (K (simp_tac (simpset_of lthy) 1));
   53.16  
   53.17      fun one_def (l as Free(n,_)) r =
   53.18            let val b = Long_Name.base_name n
   53.19 @@ -311,12 +311,12 @@
   53.20  (*************************************************************************)
   53.21  
   53.22  (* proves a block of pattern matching equations as theorems, using unfold *)
   53.23 -fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) =
   53.24 +fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) =
   53.25    let
   53.26      val tacs =
   53.27        [rtac (unfold_thm RS @{thm ssubst_lhs}) 1,
   53.28 -       asm_simp_tac (local_simpset_of lthy) 1];
   53.29 -    fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs));
   53.30 +       asm_simp_tac (simpset_of ctxt) 1];
   53.31 +    fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs));
   53.32      fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t);
   53.33    in
   53.34      map prove_eqn eqns
   53.35 @@ -399,7 +399,7 @@
   53.36                fixrec_err "function is not declared as constant in theory";
   53.37      val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
   53.38      val simp = Goal.prove_global thy [] [] eq
   53.39 -          (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]);
   53.40 +          (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
   53.41    in simp end;
   53.42  
   53.43  fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy =
    54.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Jul 23 18:44:08 2009 +0200
    54.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Jul 23 18:44:09 2009 +0200
    54.3 @@ -363,7 +363,7 @@
    54.4  val print_simpset = Toplevel.unknown_context o
    54.5    Toplevel.keep (fn state =>
    54.6      let val ctxt = Toplevel.context_of state
    54.7 -    in Pretty.writeln (Simplifier.pretty_ss ctxt (Simplifier.local_simpset_of ctxt)) end);
    54.8 +    in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end);
    54.9  
   54.10  val print_rules = Toplevel.unknown_context o
   54.11    Toplevel.keep (ContextRules.print_rules o Toplevel.context_of);
    55.1 --- a/src/Pure/Tools/find_theorems.ML	Thu Jul 23 18:44:08 2009 +0200
    55.2 +++ b/src/Pure/Tools/find_theorems.ML	Thu Jul 23 18:44:09 2009 +0200
    55.3 @@ -207,7 +207,7 @@
    55.4  
    55.5  fun filter_simp ctxt t (_, thm) =
    55.6    let
    55.7 -    val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt);
    55.8 +    val mksimps = Simplifier.mksimps (simpset_of ctxt);
    55.9      val extract_simp =
   55.10        (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl);
   55.11      val ss = is_matching_thm false extract_simp ctxt false t thm;
    56.1 --- a/src/Tools/eqsubst.ML	Thu Jul 23 18:44:08 2009 +0200
    56.2 +++ b/src/Tools/eqsubst.ML	Thu Jul 23 18:44:09 2009 +0200
    56.3 @@ -127,7 +127,7 @@
    56.4  
    56.5  (* changes object "=" to meta "==" which prepares a given rewrite rule *)
    56.6  fun prep_meta_eq ctxt =
    56.7 -  Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes;
    56.8 +  Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes;
    56.9  
   56.10  
   56.11    (* a type abriviation for match information *)
    57.1 --- a/src/ZF/IntDiv_ZF.thy	Thu Jul 23 18:44:08 2009 +0200
    57.2 +++ b/src/ZF/IntDiv_ZF.thy	Thu Jul 23 18:44:09 2009 +0200
    57.3 @@ -1732,7 +1732,7 @@
    57.4             (if ~b | #0 $<= integ_of w                    
    57.5              then integ_of v zdiv (integ_of w)     
    57.6              else (integ_of v $+ #1) zdiv (integ_of w))"
    57.7 - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
    57.8 + apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
    57.9   apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zdiv_zmult_zmult1 pos_zdiv_mult_2 lemma neg_zdiv_mult_2)
   57.10   done
   57.11  
   57.12 @@ -1778,7 +1778,7 @@
   57.13                   then #2 $* (integ_of v zmod integ_of w) $+ #1     
   57.14                   else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1   
   57.15              else #2 $* (integ_of v zmod integ_of w))"
   57.16 - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT)
   57.17 + apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT)
   57.18   apply (simp (no_asm_simp) del: bin_arith_extra_simps@bin_rel_simps add: zmod_zmult_zmult1 pos_zmod_mult_2 lemma neg_zmod_mult_2)
   57.19   done
   57.20  
    58.1 --- a/src/ZF/Tools/ind_cases.ML	Thu Jul 23 18:44:08 2009 +0200
    58.2 +++ b/src/ZF/Tools/ind_cases.ML	Thu Jul 23 18:44:09 2009 +0200
    58.3 @@ -47,8 +47,7 @@
    58.4  
    58.5  fun inductive_cases args thy =
    58.6    let
    58.7 -    val read_prop = Syntax.read_prop (ProofContext.init thy);
    58.8 -    val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop;
    58.9 +    val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy);
   58.10      val facts = args |> map (fn ((name, srcs), props) =>
   58.11        ((name, map (Attrib.attribute thy) srcs),
   58.12          map (Thm.no_attributes o single o mk_cases) props));
   58.13 @@ -62,7 +61,7 @@
   58.14      (Scan.lift (Scan.repeat1 Args.name_source) >>
   58.15        (fn props => fn ctxt =>
   58.16          props
   58.17 -        |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt))
   58.18 +        |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt))
   58.19          |> Method.erule 0))
   58.20      "dynamic case analysis on sets";
   58.21  
    59.1 --- a/src/ZF/UNITY/Constrains.thy	Thu Jul 23 18:44:08 2009 +0200
    59.2 +++ b/src/ZF/UNITY/Constrains.thy	Thu Jul 23 18:44:09 2009 +0200
    59.3 @@ -471,7 +471,7 @@
    59.4  (*proves "co" properties when the program is specified*)
    59.5  
    59.6  fun constrains_tac ctxt =
    59.7 -  let val css as (cs, ss) = local_clasimpset_of ctxt in
    59.8 +  let val css as (cs, ss) = clasimpset_of ctxt in
    59.9     SELECT_GOAL
   59.10        (EVERY [REPEAT (Always_Int_tac 1),
   59.11                REPEAT (etac @{thm Always_ConstrainsI} 1
   59.12 @@ -494,7 +494,7 @@
   59.13  
   59.14  (*For proving invariants*)
   59.15  fun always_tac ctxt i = 
   59.16 -    rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   59.17 +    rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i;
   59.18  *}
   59.19  
   59.20  setup Program_Defs.setup
    60.1 --- a/src/ZF/UNITY/SubstAx.thy	Thu Jul 23 18:44:08 2009 +0200
    60.2 +++ b/src/ZF/UNITY/SubstAx.thy	Thu Jul 23 18:44:09 2009 +0200
    60.3 @@ -351,7 +351,7 @@
    60.4  ML {*
    60.5  (*proves "ensures/leadsTo" properties when the program is specified*)
    60.6  fun ensures_tac ctxt sact =
    60.7 -  let val css as (cs, ss) = local_clasimpset_of ctxt in
    60.8 +  let val css as (cs, ss) = clasimpset_of ctxt in
    60.9      SELECT_GOAL
   60.10        (EVERY [REPEAT (Always_Int_tac 1),
   60.11                etac @{thm Always_LeadsTo_Basis} 1 
    61.1 --- a/src/ZF/int_arith.ML	Thu Jul 23 18:44:08 2009 +0200
    61.2 +++ b/src/ZF/int_arith.ML	Thu Jul 23 18:44:09 2009 +0200
    61.3 @@ -145,7 +145,7 @@
    61.4    val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys
    61.5    fun numeral_simp_tac ss =
    61.6      ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss))
    61.7 -    THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss)))
    61.8 +    THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss)))
    61.9    val simplify_meta_eq  = ArithData.simplify_meta_eq (add_0s @ mult_1s)
   61.10    end;
   61.11