# HG changeset patch # User wenzelm # Date 1248367449 -7200 # Node ID ef59550a55d32607bf70c95829a72cf898947c5b # Parent 253f6808dabe432cb5ad8eb1f7fa37742ed79d7f renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset; diff -r 253f6808dabe -r ef59550a55d3 doc-src/TutorialI/Protocol/Message.thy --- a/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/doc-src/TutorialI/Protocol/Message.thy Thu Jul 23 18:44:09 2009 +0200 @@ -915,15 +915,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o spy_analz_tac o clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o atomic_spy_analz_tac o clasimpset_of) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o local_simpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Fake_insert_simp_tac o simpset_of) *} "for debugging spy_analz" diff -r 253f6808dabe -r ef59550a55d3 doc-src/TutorialI/Protocol/Public.thy --- a/doc-src/TutorialI/Protocol/Public.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/doc-src/TutorialI/Protocol/Public.thy Thu Jul 23 18:44:09 2009 +0200 @@ -154,7 +154,7 @@ ML {* fun possibility_tac ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [used_Says])) + (ALLGOALS (simp_tac (simpset_of ctxt delsimps [used_Says])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])); diff -r 253f6808dabe -r ef59550a55d3 src/CCL/CCL.thy --- a/src/CCL/CCL.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/CCL/CCL.thy Thu Jul 23 18:44:09 2009 +0200 @@ -257,9 +257,9 @@ (mk_dstnct_rls @{theory} ["bot","true","false","pair","lambda"]) end fun mk_dstnct_thms thy defs inj_rls xs = - let fun mk_dstnct_thm rls s = prove_goalw thy defs s - (fn _ => [simp_tac (simpset_of thy addsimps (rls@inj_rls)) 1]) - in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end + let fun mk_dstnct_thm rls s = prove_goalw thy defs s + (fn _ => [simp_tac (global_simpset_of thy addsimps (rls@inj_rls)) 1]) + in map (mk_dstnct_thm ccl_dstncts) (mk_dstnct_rls thy xs) end fun mkall_dstnct_thms thy defs i_rls xss = List.concat (map (mk_dstnct_thms thy defs i_rls) xss) diff -r 253f6808dabe -r ef59550a55d3 src/CCL/Type.thy --- a/src/CCL/Type.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/CCL/Type.thy Thu Jul 23 18:44:09 2009 +0200 @@ -132,10 +132,10 @@ fun mk_ncanT_tac ctxt defs top_crls crls s = prove_goalw (ProofContext.theory_of ctxt) defs s (fn major::prems => [(resolve_tac ([major] RL top_crls) 1), (REPEAT_SOME (eresolve_tac (crls @ [exE,bexE,conjE,disjE]))), - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt))), + (ALLGOALS (asm_simp_tac (simpset_of ctxt))), (ALLGOALS (ares_tac (prems RL [lemma]) ORELSE' etac bspec )), - (safe_tac (local_claset_of ctxt addSIs prems))]) + (safe_tac (claset_of ctxt addSIs prems))]) end *} @@ -408,7 +408,7 @@ fun mk_genIs thy defs genXH gen_mono s = prove_goalw thy defs s (fn prems => [rtac (genXH RS iffD2) 1, - simp_tac (simpset_of thy) 1, + simp_tac (global_simpset_of thy) 1, TRY (fast_tac (@{claset} addIs ([genXH RS iffD2,gen_mono RS coinduct3_mono_lemma RS lfpI] @ prems)) 1)]) @@ -442,7 +442,7 @@ "[| : lfp(%x. POgen(x) Un R Un PO); : lfp(%x. POgen(x) Un R Un PO) |] ==> : POgen(lfp(%x. POgen(x) Un R Un PO))"]; fun POgen_tac ctxt (rla,rlb) i = - SELECT_GOAL (safe_tac (local_claset_of ctxt)) i THEN + SELECT_GOAL (safe_tac (claset_of ctxt)) i THEN rtac (rlb RS (rla RS @{thm ssubst_pair})) i THEN (REPEAT (resolve_tac (POgenIs @ [@{thm PO_refl} RS (@{thm POgen_mono} RS ci3_AI)] @ (POgenIs RL [@{thm POgen_mono} RS ci3_AgenI]) @ [@{thm POgen_mono} RS ci3_RI]) i)); @@ -481,9 +481,9 @@ fun EQgen_tac ctxt rews i = SELECT_GOAL - (TRY (safe_tac (local_claset_of ctxt)) THEN + (TRY (safe_tac (claset_of ctxt)) THEN resolve_tac ((rews@[refl]) RL ((rews@[refl]) RL [@{thm ssubst_pair}])) i THEN - ALLGOALS (simp_tac (local_simpset_of ctxt)) THEN + ALLGOALS (simp_tac (simpset_of ctxt)) THEN ALLGOALS EQgen_raw_tac) i *} diff -r 253f6808dabe -r ef59550a55d3 src/FOL/cladata.ML --- a/src/FOL/cladata.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/FOL/cladata.ML Thu Jul 23 18:44:09 2009 +0200 @@ -19,7 +19,7 @@ structure Cla = ClassicalFun(Classical_Data); structure BasicClassical: BASIC_CLASSICAL = Cla; open BasicClassical; -ML_Antiquote.value "claset" (Scan.succeed "Cla.local_claset_of (ML_Context.the_local_context ())"); +ML_Antiquote.value "claset" (Scan.succeed "Cla.claset_of (ML_Context.the_local_context ())"); (*Propositional rules*) diff -r 253f6808dabe -r ef59550a55d3 src/FOL/simpdata.ML --- a/src/FOL/simpdata.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/FOL/simpdata.ML Thu Jul 23 18:44:09 2009 +0200 @@ -164,6 +164,6 @@ open Clasimp; ML_Antiquote.value "clasimpset" - (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"); + (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())"); val FOL_css = (FOL_cs, FOL_ss); diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Message.thy --- a/src/HOL/Auth/Message.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Message.thy Thu Jul 23 18:44:09 2009 +0200 @@ -939,15 +939,15 @@ lemmas Fake_parts_sing_imp_Un = Fake_parts_sing [THEN [2] rev_subsetD] method_setup spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Message.spy_analz_tac o clasimpset_of) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* - Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o local_clasimpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Message.atomic_spy_analz_tac o clasimpset_of) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* - Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o local_simpset_of) *} + Scan.succeed (SIMPLE_METHOD' o Message.Fake_insert_simp_tac o simpset_of) *} "for debugging spy_analz" end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Public.thy --- a/src/HOL/Auth/Public.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Public.thy Thu Jul 23 18:44:09 2009 +0200 @@ -407,7 +407,7 @@ (*Tactic for possibility theorems*) fun possibility_tac ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}])) + (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])) @@ -416,7 +416,7 @@ nonces and keys initially*) fun basic_possibility_tac ctxt = REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Shared.thy --- a/src/HOL/Auth/Shared.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Shared.thy Thu Jul 23 18:44:09 2009 +0200 @@ -204,7 +204,7 @@ such as Nonce ?N \ used evs that match Nonce_supply*) fun possibility_tac ctxt = (REPEAT - (ALLGOALS (simp_tac (local_simpset_of ctxt + (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}] setSolver safe_solver)) THEN @@ -215,7 +215,7 @@ nonces and keys initially*) fun basic_possibility_tac ctxt = REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Smartcard/ShoupRubin.thy --- a/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubin.thy Thu Jul 23 18:44:09 2009 +0200 @@ -757,7 +757,7 @@ (*SR9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN - (*Base*) (force_tac (local_clasimpset_of ctxt)) 1 + (*Base*) (force_tac (clasimpset_of ctxt)) 1 val analz_prepare_tac = prepare_tac THEN diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Smartcard/ShoupRubinBella.thy --- a/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Smartcard/ShoupRubinBella.thy Thu Jul 23 18:44:09 2009 +0200 @@ -755,7 +755,7 @@ fun prepare_tac ctxt = (*SR_U8*) forward_tac [@{thm Outpts_B_Card_form_7}] 14 THEN - (*SR_U8*) clarify_tac (local_claset_of ctxt) 15 THEN + (*SR_U8*) clarify_tac (claset_of ctxt) 15 THEN (*SR_U9*) forward_tac [@{thm Outpts_A_Card_form_4}] 16 THEN (*SR_U11*) forward_tac [@{thm Outpts_A_Card_form_10}] 21 @@ -765,7 +765,7 @@ (*SR_U9*) dresolve_tac [@{thm Gets_imp_knows_Spy_parts_Snd}] 19 THEN (*Oops1*) dresolve_tac [@{thm Outpts_B_Card_form_7}] 25 THEN (*Oops2*) dresolve_tac [@{thm Outpts_A_Card_form_10}] 27 THEN - (*Base*) (force_tac (local_clasimpset_of ctxt)) 1 + (*Base*) (force_tac (clasimpset_of ctxt)) 1 fun analz_prepare_tac ctxt = prepare_tac ctxt THEN diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Auth/Smartcard/Smartcard.thy --- a/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Auth/Smartcard/Smartcard.thy Thu Jul 23 18:44:09 2009 +0200 @@ -375,7 +375,7 @@ such as Nonce ?N \ used evs that match Nonce_supply*) fun possibility_tac ctxt = (REPEAT - (ALLGOALS (simp_tac (local_simpset_of ctxt + (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}, @{thm used_Gets}, @{thm used_Inputs}, @{thm used_C_Gets}, @{thm used_Outpts}, @{thm used_A_Gets}] setSolver safe_solver)) @@ -387,7 +387,7 @@ nonces and keys initially*) fun basic_possibility_tac ctxt = REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Bali/Basis.thy --- a/src/HOL/Bali/Basis.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Bali/Basis.thy Thu Jul 23 18:44:09 2009 +0200 @@ -229,7 +229,7 @@ ML {* fun sum3_instantiate ctxt thm = map (fn s => - simplify (Simplifier.local_simpset_of ctxt delsimps[@{thm not_None_eq}]) + simplify (simpset_of ctxt delsimps[@{thm not_None_eq}]) (read_instantiate ctxt [(("t", 0), "In" ^ s ^ " ?x")] thm)) ["1l","2","3","1r"] *} (* e.g. lemmas is_stmt_rews = is_stmt_def [of "In1l x", simplified] *) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Decision_Procs/Dense_Linear_Order.thy --- a/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Decision_Procs/Dense_Linear_Order.thy Thu Jul 23 18:44:09 2009 +0200 @@ -692,7 +692,7 @@ val clt = Thm.dest_fun2 ct val cz = Thm.dest_arg ct val neg = cr - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} "verification condition generator plus simplification" end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Hoare/HoareAbort.thy --- a/src/HOL/Hoare/HoareAbort.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Hoare/HoareAbort.thy Thu Jul 23 18:44:09 2009 +0200 @@ -251,7 +251,7 @@ method_setup vcg_simp = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (local_simpset_of ctxt)))) *} + SIMPLE_METHOD' (hoare_tac ctxt (asm_full_simp_tac (simpset_of ctxt)))) *} "verification condition generator plus simplification" (* Special syntax for guarded statements and guarded array updates: *) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Hoare/hoare_tac.ML --- a/src/HOL/Hoare/hoare_tac.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Hoare/hoare_tac.ML Thu Jul 23 18:44:09 2009 +0200 @@ -73,7 +73,7 @@ val MsetT = fastype_of big_Collect; fun Mset_incl t = mk_Trueprop (inclt MsetT $ Free (Mset, MsetT) $ t); val impl = Logic.mk_implies (Mset_incl big_Collect, Mset_incl small_Collect); - val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (local_claset_of ctxt) 1); + val th = Goal.prove ctxt [Mset, P] [] impl (fn _ => blast_tac (claset_of ctxt) 1); in (vars, th) end; end; diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Library/comm_ring.ML --- a/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Library/comm_ring.ML Thu Jul 23 18:44:09 2009 +0200 @@ -89,7 +89,7 @@ fun comm_ring_tac ctxt = SUBGOAL (fn (g, i) => let val thy = ProofContext.theory_of ctxt; - val cring_ss = Simplifier.local_simpset_of ctxt (*FIXME really the full simpset!?*) + val cring_ss = Simplifier.simpset_of ctxt (*FIXME really the full simpset!?*) addsimps cring_simps; val (ca, cvs, clhs, crhs) = reif_eq thy (HOLogic.dest_Trueprop g) val norm_eq_th = diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Library/reflection.ML --- a/src/HOL/Library/reflection.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Library/reflection.ML Thu Jul 23 18:44:09 2009 +0200 @@ -285,7 +285,7 @@ val th' = instantiate ([], cvs) th val t' = (fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of) th' val th'' = Goal.prove ctxt [] [] (HOLogic.mk_Trueprop (HOLogic.mk_eq (t, t'))) - (fn _ => simp_tac (local_simpset_of ctxt) 1) + (fn _ => simp_tac (simpset_of ctxt) 1) in FWD trans [th'',th'] end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/MicroJava/J/JTypeSafe.thy --- a/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/MicroJava/J/JTypeSafe.thy Thu Jul 23 18:44:09 2009 +0200 @@ -204,7 +204,7 @@ apply( simp_all) apply( tactic "ALLGOALS strip_tac") apply( tactic {* ALLGOALS (eresolve_tac [thm "ty_expr.cases", thm "ty_exprs.cases", thm "wt_stmt.cases"] - THEN_ALL_NEW (full_simp_tac (simpset_of @{theory Conform}))) *}) + THEN_ALL_NEW (full_simp_tac (global_simpset_of @{theory Conform}))) *}) apply(tactic "ALLGOALS (EVERY' [REPEAT o (etac conjE), REPEAT o hyp_subst_tac])") -- "Level 7" diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Modelcheck/mucke_oracle.ML --- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Jul 23 18:44:09 2009 +0200 @@ -109,7 +109,7 @@ ( OldGoals.push_proof(); OldGoals.goalw_cterm [] (cterm_of sign trm); -by (simp_tac (simpset_of sign) 1); +by (simp_tac (global_simpset_of sign) 1); let val if_tmp_result = result() in diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Nominal/nominal_datatype.ML --- a/src/HOL/Nominal/nominal_datatype.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jul 23 18:44:09 2009 +0200 @@ -324,7 +324,7 @@ (perm_names_types ~~ perm_indnames)))) (fn _ => EVERY [indtac induction perm_indnames 1, ALLGOALS (asm_full_simp_tac - (simpset_of thy2 addsimps [perm_fun_def]))])), + (global_simpset_of thy2 addsimps [perm_fun_def]))])), length new_type_names)); (**** prove [] \ t = t ****) @@ -344,7 +344,7 @@ (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) (fn _ => EVERY [indtac induction perm_indnames 1, - ALLGOALS (asm_full_simp_tac (simpset_of thy2))])), + ALLGOALS (asm_full_simp_tac (global_simpset_of thy2))])), length new_type_names)) end) atoms); @@ -379,7 +379,7 @@ (perm_names ~~ map body_type perm_types ~~ perm_indnames))))) (fn _ => EVERY [indtac induction perm_indnames 1, - ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt2', pt2_ax]))]))), + ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt2', pt2_ax]))]))), length new_type_names) end) atoms); @@ -415,7 +415,7 @@ (perm_names ~~ map body_type perm_types ~~ perm_indnames)))))) (fn _ => EVERY [indtac induction perm_indnames 1, - ALLGOALS (asm_full_simp_tac (simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))), + ALLGOALS (asm_full_simp_tac (global_simpset_of thy2 addsimps [pt3', pt3_rev', pt3_ax]))]))), length new_type_names) end) atoms); @@ -437,7 +437,7 @@ val permT2 = mk_permT (Type (name2, [])); val Ts = map body_type perm_types; val cp_inst = cp_inst_of thy name1 name2; - val simps = simpset_of thy addsimps (perm_fun_def :: + val simps = global_simpset_of thy addsimps (perm_fun_def :: (if name1 <> name2 then let val dj = dj_thm_of thy name2 name1 in [dj RS (cp_inst RS dj_cp), dj RS dj_perm_perm_forget] end @@ -601,7 +601,7 @@ end) (rep_set_names'' ~~ recTs' ~~ perm_indnames'))))) (fn _ => EVERY [indtac rep_induct [] 1, - ALLGOALS (simp_tac (simpset_of thy4 addsimps + ALLGOALS (simp_tac (global_simpset_of thy4 addsimps (symmetric perm_fun_def :: abs_perm))), ALLGOALS (resolve_tac rep_intrs THEN_ALL_NEW assume_tac)])), length new_type_names)); @@ -661,8 +661,8 @@ map (inter_sort thy sort o snd) tvs, [pt_class]) (EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], - asm_full_simp_tac (simpset_of thy addsimps [Rep_inverse]) 1, - asm_full_simp_tac (simpset_of thy addsimps + asm_full_simp_tac (global_simpset_of thy addsimps [Rep_inverse]) 1, + asm_full_simp_tac (global_simpset_of thy addsimps [Rep RS perm_closed RS Abs_inverse]) 1, asm_full_simp_tac (HOL_basic_ss addsimps [PureThy.get_thm thy ("pt_" ^ Long_Name.base_name atom ^ "3")]) 1]) thy @@ -690,7 +690,7 @@ map (inter_sort thy sort o snd) tvs, [cp_class]) (EVERY [Class.intro_classes_tac [], rewrite_goals_tac [perm_def], - asm_full_simp_tac (simpset_of thy addsimps + asm_full_simp_tac (global_simpset_of thy addsimps ((Rep RS perm_closed1 RS Abs_inverse) :: (if atom1 = atom2 then [] else [Rep RS perm_closed2 RS Abs_inverse]))) 1, @@ -875,7 +875,7 @@ | prove_distinct_thms (p as (rep_thms, dist_lemma)) (k, t :: ts) = let val dist_thm = Goal.prove_global thy8 [] [] t (fn _ => - simp_tac (simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) + simp_tac (global_simpset_of thy8 addsimps (dist_lemma :: rep_thms)) 1) in dist_thm :: standard (dist_thm RS not_sym) :: prove_distinct_thms p (k, ts) end; @@ -920,7 +920,7 @@ (HOLogic.mk_Trueprop (HOLogic.mk_eq (perm (list_comb (c, l_args)), list_comb (c, r_args))))) (fn _ => EVERY - [simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, + [simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: perm_defs)) 1, simp_tac (HOL_basic_ss addsimps (Rep_thms @ Abs_inverse_thms @ constr_defs @ perm_closed_thms)) 1, TRY (simp_tac (HOL_basic_ss addsimps @@ -973,7 +973,7 @@ (HOLogic.mk_eq (list_comb (c, args1), list_comb (c, args2)), foldr1 HOLogic.mk_conj eqs)))) (fn _ => EVERY - [asm_full_simp_tac (simpset_of thy8 addsimps (constr_rep_thm :: + [asm_full_simp_tac (global_simpset_of thy8 addsimps (constr_rep_thm :: rep_inject_thms')) 1, TRY (asm_full_simp_tac (HOL_basic_ss addsimps (fresh_def :: supp_def :: alpha @ abs_perm @ abs_fresh @ rep_inject_thms @ @@ -1100,7 +1100,7 @@ (Const ("Nominal.supp", T --> HOLogic.mk_setT atomT) $ Free (s, T))) (indnames ~~ recTs))))) (fn _ => indtac dt_induct indnames 1 THEN - ALLGOALS (asm_full_simp_tac (simpset_of thy8 addsimps + ALLGOALS (asm_full_simp_tac (global_simpset_of thy8 addsimps (abs_supp @ supp_atm @ PureThy.get_thms thy8 ("fs_" ^ Long_Name.base_name atom ^ "1") @ List.concat supp_thms))))), diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Nominal/nominal_fresh_fun.ML --- a/src/HOL/Nominal/nominal_fresh_fun.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_fresh_fun.ML Thu Jul 23 18:44:09 2009 +0200 @@ -143,7 +143,7 @@ let val thy = theory_of_thm thm; val ctx = Context.init_proof thy; - val ss = simpset_of thy; + val ss = global_simpset_of thy; val abs_fresh = PureThy.get_thms thy "abs_fresh"; val fresh_perm_app = PureThy.get_thms thy "fresh_perm_app"; val ss' = ss addsimps fresh_prod::abs_fresh; diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Thu Jul 23 18:44:09 2009 +0200 @@ -403,7 +403,7 @@ cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN - asm_full_simp_tac (simpset_of thy) 1) + asm_full_simp_tac (simpset_of ctxt) 1) end) |> singleton (ProofContext.export ctxt' ctxt); (** strong case analysis rule **) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Thu Jul 23 18:44:09 2009 +0200 @@ -438,7 +438,7 @@ cut_facts_tac [th] 1 THEN REPEAT (etac conjE 1) THEN REPEAT (REPEAT (resolve_tac [conjI, impI] 1) THEN etac impE 1 THEN atac 1 THEN REPEAT (etac @{thm allE_Nil} 1) THEN - asm_full_simp_tac (simpset_of thy) 1) + asm_full_simp_tac (simpset_of ctxt) 1) end) |> fresh_postprocess |> singleton (ProofContext.export ctxt' ctxt); diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Nominal/nominal_permeq.ML --- a/src/HOL/Nominal/nominal_permeq.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jul 23 18:44:09 2009 +0200 @@ -404,19 +404,19 @@ Method.sections (Simplifier.simp_modifiers') >> (fn (prems, tac) => fn ctxt => METHOD (fn facts => HEADGOAL (Method.insert_tac (prems @ facts) THEN' - (CHANGED_PROP oo tac) (local_simpset_of ctxt)))); + (CHANGED_PROP oo tac) (simpset_of ctxt)))); (* setup so that the simpset is used which is active at the moment when the tactic is called *) fun local_simp_meth_setup tac = Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> - (K (SIMPLE_METHOD' o tac o local_simpset_of)); + (K (SIMPLE_METHOD' o tac o simpset_of)); (* uses HOL_basic_ss only and fails if the tactic does not solve the subgoal *) fun basic_simp_meth_setup debug tac = Scan.depend (fn ctxt => Scan.succeed (Simplifier.map_ss (fn _ => HOL_basic_ss) ctxt, ())) -- Method.sections (Simplifier.simp_modifiers' @ Splitter.split_modifiers) >> - (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o local_simpset_of)); + (K (SIMPLE_METHOD' o (fn ss => if debug then tac ss else SOLVEI (tac ss)) o simpset_of)); val perm_simp_meth_debug = local_simp_meth_setup dperm_simp_tac; val perm_extend_simp_meth = local_simp_meth_setup perm_extend_simp_tac; diff -r 253f6808dabe -r ef59550a55d3 src/HOL/SET-Protocol/MessageSET.thy --- a/src/HOL/SET-Protocol/MessageSET.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/SET-Protocol/MessageSET.thy Thu Jul 23 18:44:09 2009 +0200 @@ -939,17 +939,17 @@ method_setup spy_analz = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.spy_analz_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.spy_analz_tac (clasimpset_of ctxt))) *} "for proving the Fake case when analz is involved" method_setup atomic_spy_analz = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.atomic_spy_analz_tac (clasimpset_of ctxt))) *} "for debugging spy_analz" method_setup Fake_insert_simp = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (local_simpset_of ctxt))) *} + SIMPLE_METHOD' (MessageSET.Fake_insert_simp_tac (simpset_of ctxt))) *} "for debugging spy_analz" end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/SET-Protocol/PublicSET.thy --- a/src/HOL/SET-Protocol/PublicSET.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/SET-Protocol/PublicSET.thy Thu Jul 23 18:44:09 2009 +0200 @@ -350,7 +350,7 @@ (*Tactic for possibility theorems*) fun possibility_tac ctxt = REPEAT (*omit used_Says so that Nonces start from different traces!*) - (ALLGOALS (simp_tac (local_simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}])) + (ALLGOALS (simp_tac (simpset_of ctxt delsimps [@{thm used_Says}, @{thm used_Notes}])) THEN REPEAT_FIRST (eq_assume_tac ORELSE' resolve_tac [refl, conjI, @{thm Nonce_supply}])) @@ -359,7 +359,7 @@ nonces and keys initially*) fun basic_possibility_tac ctxt = REPEAT - (ALLGOALS (asm_simp_tac (local_simpset_of ctxt setSolver safe_solver)) + (ALLGOALS (asm_simp_tac (simpset_of ctxt setSolver safe_solver)) THEN REPEAT_FIRST (resolve_tac [refl, conjI])) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/SizeChange/sct.ML --- a/src/HOL/SizeChange/sct.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/SizeChange/sct.ML Thu Jul 23 18:44:09 2009 +0200 @@ -184,7 +184,7 @@ fun setup_probe_goal ctxt domT Dtab Mtab (i, j) = let - val css = local_clasimpset_of ctxt + val css = clasimpset_of ctxt val thy = ProofContext.theory_of ctxt val RD1 = get_elem (Dtab i) val RD2 = get_elem (Dtab j) @@ -269,7 +269,7 @@ fun in_graph_tac ctxt = simp_tac (HOL_basic_ss addsimps has_edge_simps) 1 - THEN (simp_tac (local_simpset_of ctxt) 1) (* FIXME reduce simpset *) + THEN (simp_tac (simpset_of ctxt) 1) (* FIXME reduce simpset *) fun approx_tac _ (NoStep thm) = rtac disjI1 1 THEN rtac thm 1 | approx_tac ctxt (Graph (G, thm)) = @@ -334,7 +334,7 @@ val sound_int_goal = HOLogic.mk_Trueprop (mk_sound_int ACG RDlist mfuns) val tac = - unfold_tac [sound_int_def, len_simp] (local_simpset_of ctxt) + unfold_tac [sound_int_def, len_simp] (simpset_of ctxt) THEN all_less_tac (map (all_less_tac o map (approx_tac ctxt)) parts) in tac (instantiate' [] [SOME (cterm_of thy ACG), SOME (cterm_of thy mfuns)] st) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/TLA/Memory/MemoryImplementation.thy --- a/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/TLA/Memory/MemoryImplementation.thy Thu Jul 23 18:44:09 2009 +0200 @@ -763,7 +763,7 @@ *) ML {* fun split_idle_tac ctxt simps i = - let val ss = Simplifier.local_simpset_of ctxt in + let val ss = simpset_of ctxt in TRY (rtac @{thm actionI} i) THEN InductTacs.case_tac ctxt "(s,t) |= unchanged (e p, c p, r p, m p, rmhist!p)" i THEN rewrite_goals_tac @{thms action_rews} THEN diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/decompose.ML --- a/src/HOL/Tools/Function/decompose.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/decompose.ML Thu Jul 23 18:44:09 2009 +0200 @@ -98,7 +98,7 @@ fun auto_decompose_tac ctxt = Termination.TERMINATION ctxt - (decompose_tac ctxt (auto_tac (local_clasimpset_of ctxt)) + (decompose_tac ctxt (auto_tac (clasimpset_of ctxt)) (K (K all_tac)) (K (K no_tac))) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/fundef_core.ML --- a/src/HOL/Tools/Function/fundef_core.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/fundef_core.ML Thu Jul 23 18:44:09 2009 +0200 @@ -702,7 +702,7 @@ Goal.init goal |> (SINGLE (resolve_tac [accI] 1)) |> the |> (SINGLE (eresolve_tac [Thm.forall_elim_vars 0 R_cases] 1)) |> the - |> (SINGLE (auto_tac (local_clasimpset_of ctxt))) |> the + |> (SINGLE (auto_tac (clasimpset_of ctxt))) |> the |> Goal.conclude |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end @@ -831,7 +831,7 @@ ((rtac (G_induct OF [a])) THEN_ALL_NEW (rtac accI) THEN_ALL_NEW (etac R_cases) - THEN_ALL_NEW (asm_full_simp_tac (local_simpset_of octxt))) 1) + THEN_ALL_NEW (asm_full_simp_tac (simpset_of octxt))) 1) val default_thm = (forall_intr_vars graph_implies_dom) COMP (f_def COMP fundef_default_value) @@ -849,9 +849,9 @@ (fn _ => rtac (instantiate' [] [SOME (cterm_of thy lhs_acc)] case_split) 1 THEN (rtac (Thm.forall_elim_vars 0 psimp) THEN_ALL_NEW assume_tac) 1 - THEN (simp_default_tac (local_simpset_of ctxt) 1) + THEN (simp_default_tac (simpset_of ctxt) 1) THEN (etac not_acc_down 1) - THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (local_simpset_of ctxt))) 1) + THEN ((etac R_cases) THEN_ALL_NEW (simp_default_tac (simpset_of ctxt))) 1) |> fold_rev forall_intr_rename (map fst oqs ~~ cqs) end in diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 18:44:09 2009 +0200 @@ -217,7 +217,7 @@ fun lexicographic_order_tac ctxt = TRY (FundefCommon.apply_termination_rule ctxt 1) THEN lex_order_tac ctxt - (auto_tac (local_clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt)) + (auto_tac (clasimpset_of ctxt addsimps2 FundefCommon.Termination_Simps.get ctxt)) val lexicographic_order = SIMPLE_METHOD o lexicographic_order_tac diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/mutual.ML --- a/src/HOL/Tools/Function/mutual.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/mutual.ML Thu Jul 23 18:44:09 2009 +0200 @@ -206,7 +206,7 @@ (HOLogic.Trueprop $ HOLogic.mk_eq (list_comb (f, args), rhs)) (fn _ => (LocalDefs.unfold_tac ctxt all_orig_fdefs) THEN EqSubst.eqsubst_tac ctxt [0] [simp] 1 - THEN (simp_tac (local_simpset_of ctxt addsimps SumTree.proj_in_rules)) 1) + THEN (simp_tac (simpset_of ctxt addsimps SumTree.proj_in_rules)) 1) |> restore_cond |> export end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/scnp_reconstruct.ML --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Thu Jul 23 18:44:09 2009 +0200 @@ -291,7 +291,7 @@ THEN (rtac @{thm rp_inv_image_rp} 1) THEN (rtac (order_rpair ms_rp label) 1) THEN PRIMITIVE (instantiate' [] [SOME level_mapping]) - THEN unfold_tac @{thms rp_inv_image_def} (local_simpset_of ctxt) + THEN unfold_tac @{thms rp_inv_image_def} (simpset_of ctxt) THEN LocalDefs.unfold_tac ctxt (@{thms split_conv} @ @{thms fst_conv} @ @{thms snd_conv}) THEN REPEAT (SOMEGOAL (resolve_tac [@{thm Un_least}, @{thm empty_subsetI}])) @@ -406,7 +406,7 @@ fun decomp_scnp orders ctxt = let val extra_simps = FundefCommon.Termination_Simps.get ctxt - val autom_tac = auto_tac (local_clasimpset_of ctxt addsimps2 extra_simps) + val autom_tac = auto_tac (clasimpset_of ctxt addsimps2 extra_simps) in SIMPLE_METHOD (gen_sizechange_tac orders autom_tac ctxt (print_error ctxt)) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Function/termination.ML --- a/src/HOL/Tools/Function/termination.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Function/termination.ML Thu Jul 23 18:44:09 2009 +0200 @@ -303,7 +303,7 @@ THEN' ((rtac @{thm refl}) (* unification instantiates all Vars *) ORELSE' ((rtac @{thm conjI}) THEN' (rtac @{thm refl}) - THEN' (blast_tac (local_claset_of ctxt)))) (* Solve rest of context... not very elegant *) + THEN' (blast_tac (claset_of ctxt)))) (* Solve rest of context... not very elegant *) ) i in ((PRIMITIVE (Drule.cterm_instantiate [(cert rel, cert relation)]) diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/Qelim/ferrante_rackoff.ML --- a/src/HOL/Tools/Qelim/ferrante_rackoff.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff.ML Thu Jul 23 18:44:09 2009 +0200 @@ -228,6 +228,6 @@ ObjectLogic.full_atomize_tac i THEN simp_tac (#simpset (snd instance)) i THEN (* FIXME already part of raw_ferrack_qe_conv? *) CONVERSION (ObjectLogic.judgment_conv (raw_ferrack_qe_conv ctxt instance)) i THEN - simp_tac (Simplifier.local_simpset_of ctxt) i)); (* FIXME really? *) + simp_tac (simpset_of ctxt) i)); (* FIXME really? *) end; diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/inductive.ML --- a/src/HOL/Tools/inductive.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/inductive.ML Thu Jul 23 18:44:09 2009 +0200 @@ -425,7 +425,7 @@ fun mk_cases ctxt prop = let val thy = ProofContext.theory_of ctxt; - val ss = Simplifier.local_simpset_of ctxt; + val ss = simpset_of ctxt; fun err msg = error (Pretty.string_of (Pretty.block diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/recdef.ML --- a/src/HOL/Tools/recdef.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/recdef.ML Thu Jul 23 18:44:09 2009 +0200 @@ -172,15 +172,15 @@ NONE => ctxt0 | SOME src => #2 (Method.syntax (Method.sections recdef_modifiers) src ctxt0)); val {simps, congs, wfs} = get_hints ctxt; - val cs = local_claset_of ctxt; - val ss = local_simpset_of ctxt addsimps simps; + val cs = claset_of ctxt; + val ss = simpset_of ctxt addsimps simps; in (cs, ss, rev (map snd congs), wfs) end; fun prepare_hints_i thy () = let val ctxt0 = ProofContext.init thy; val {simps, congs, wfs} = get_global_hints thy; - in (local_claset_of ctxt0, local_simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end; + in (claset_of ctxt0, simpset_of ctxt0 addsimps simps, rev (map snd congs), wfs) end; diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Tools/simpdata.ML --- a/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Tools/simpdata.ML Thu Jul 23 18:44:09 2009 +0200 @@ -158,7 +158,7 @@ open Clasimp; val _ = ML_Antiquote.value "clasimpset" - (Scan.succeed "Clasimp.local_clasimpset_of (ML_Context.the_local_context ())"); + (Scan.succeed "Clasimp.clasimpset_of (ML_Context.the_local_context ())"); val mksimps_pairs = [("op -->", [@{thm mp}]), ("op &", [@{thm conjunct1}, @{thm conjunct2}]), diff -r 253f6808dabe -r ef59550a55d3 src/HOL/UNITY/Comp/Alloc.thy --- a/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/UNITY/Comp/Alloc.thy Thu Jul 23 18:44:09 2009 +0200 @@ -321,7 +321,7 @@ *} method_setup record_auto = {* - Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (local_clasimpset_of ctxt))) + Scan.succeed (fn ctxt => SIMPLE_METHOD (record_auto_tac (clasimpset_of ctxt))) *} "" lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc" @@ -714,7 +714,7 @@ method_setup rename_client_map = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD (rename_client_map_tac (local_simpset_of ctxt))) + SIMPLE_METHOD (rename_client_map_tac (simpset_of ctxt))) *} "" text{*Lifting @{text Client_Increasing} to @{term systemState}*} diff -r 253f6808dabe -r ef59550a55d3 src/HOL/UNITY/Simple/NSP_Bad.thy --- a/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Thu Jul 23 18:44:09 2009 +0200 @@ -125,7 +125,7 @@ method_setup ns_induct = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (ns_induct_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (ns_induct_tac (clasimpset_of ctxt))) *} "for inductive reasoning about the Needham-Schroeder protocol" text{*Converts invariants into statements about reachable states*} diff -r 253f6808dabe -r ef59550a55d3 src/HOL/UNITY/UNITY_Main.thy --- a/src/HOL/UNITY/UNITY_Main.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/UNITY/UNITY_Main.thy Thu Jul 23 18:44:09 2009 +0200 @@ -11,12 +11,12 @@ method_setup safety = {* Scan.succeed (fn ctxt => - SIMPLE_METHOD' (constrains_tac (local_clasimpset_of ctxt))) *} + SIMPLE_METHOD' (constrains_tac (clasimpset_of ctxt))) *} "for proving safety properties" method_setup ensures_tac = {* Args.goal_spec -- Scan.lift Args.name_source >> - (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (local_clasimpset_of ctxt) s)) + (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac (clasimpset_of ctxt) s)) *} "for proving progress properties" end diff -r 253f6808dabe -r ef59550a55d3 src/HOL/Word/WordArith.thy --- a/src/HOL/Word/WordArith.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOL/Word/WordArith.thy Thu Jul 23 18:44:09 2009 +0200 @@ -513,8 +513,8 @@ fun uint_arith_tacs ctxt = let fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; - val cs = local_claset_of ctxt; - val ss = local_simpset_of ctxt; + val cs = claset_of ctxt; + val ss = simpset_of ctxt; in [ clarify_tac cs 1, full_simp_tac (uint_arith_ss_of ss) 1, @@ -1075,8 +1075,8 @@ fun unat_arith_tacs ctxt = let fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty; - val cs = local_claset_of ctxt; - val ss = local_simpset_of ctxt; + val cs = claset_of ctxt; + val ss = simpset_of ctxt; in [ clarify_tac cs 1, full_simp_tac (unat_arith_ss_of ss) 1, diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/FOCUS/Buffer.thy --- a/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/FOCUS/Buffer.thy Thu Jul 23 18:44:09 2009 +0200 @@ -101,7 +101,7 @@ fun B_prover s tac eqs = let val thy = the_context () in prove_goal thy s (fn prems => [cut_facts_tac prems 1, - tac 1, auto_tac (claset_of thy, simpset_of thy addsimps eqs)]) + tac 1, auto_tac (global_claset_of thy, global_simpset_of thy addsimps eqs)]) end; fun prove_forw s thm = B_prover s (dtac (thm RS iffD1)) []; diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/IOA/Modelcheck/MuIOA.thy --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jul 23 18:44:09 2009 +0200 @@ -278,14 +278,14 @@ by (REPEAT (rtac impI 1)); by (REPEAT (dtac eq_reflection 1)); (* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *) -by (full_simp_tac ((simpset_of sign delcongs (if_weak_cong :: weak_case_congs) +by (full_simp_tac ((global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @ rename_simps @ ioa_simps @ asig_simps)) 1); by (full_simp_tac (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); by (REPEAT (if_full_simp_tac - (simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); + (global_simpset_of sign delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1)); by (call_mucke_tac 1); (* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *) by (atac 1); diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/IOA/meta_theory/Abstraction.thy --- a/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/Abstraction.thy Thu Jul 23 18:44:09 2009 +0200 @@ -605,7 +605,7 @@ ML {* fun abstraction_tac ctxt = - let val (cs, ss) = local_clasimpset_of ctxt in + let val (cs, ss) = clasimpset_of ctxt in SELECT_GOAL (auto_tac (cs addSIs @{thms weak_strength_lemmas}, ss addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}])) end diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/IOA/meta_theory/CompoScheds.thy --- a/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/CompoScheds.thy Thu Jul 23 18:44:09 2009 +0200 @@ -299,10 +299,10 @@ in fun mkex_induct_tac ctxt sch exA exB = - let val ss = Simplifier.local_simpset_of ctxt in + let val ss = simpset_of ctxt in EVERY1[Seq_induct_tac ctxt sch defs, asm_full_simp_tac ss, - SELECT_GOAL (safe_tac (claset_of @{theory Fun})), + SELECT_GOAL (safe_tac (global_claset_of @{theory Fun})), Seq_case_simp_tac ctxt exA, Seq_case_simp_tac ctxt exB, asm_full_simp_tac ss, diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/IOA/meta_theory/Sequence.thy --- a/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/IOA/meta_theory/Sequence.thy Thu Jul 23 18:44:09 2009 +0200 @@ -1091,7 +1091,7 @@ (* on a>>s only simp_tac, as full_simp_tac is uncomplete and often causes errors *) fun Seq_case_simp_tac ctxt s i = - let val ss = Simplifier.local_simpset_of ctxt in + let val ss = simpset_of ctxt in Seq_case_tac ctxt s i THEN asm_simp_tac ss (i+2) THEN asm_full_simp_tac ss (i+1) @@ -1100,7 +1100,7 @@ (* rws are definitions to be unfolded for admissibility check *) fun Seq_induct_tac ctxt s rws i = - let val ss = Simplifier.local_simpset_of ctxt in + let val ss = simpset_of ctxt in res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i THEN (REPEAT_DETERM (CHANGED (asm_simp_tac ss (i+1)))) THEN simp_tac (ss addsimps rws) i @@ -1108,15 +1108,15 @@ fun Seq_Finite_induct_tac ctxt i = etac @{thm Seq_Finite_ind} i - THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (Simplifier.local_simpset_of ctxt) i))); + THEN (REPEAT_DETERM (CHANGED (asm_simp_tac (simpset_of ctxt) i))); fun pair_tac ctxt s = res_inst_tac ctxt [(("p", 0), s)] PairE - THEN' hyp_subst_tac THEN' asm_full_simp_tac (Simplifier.local_simpset_of ctxt); + THEN' hyp_subst_tac THEN' asm_full_simp_tac (simpset_of ctxt); (* induction on a sequence of pairs with pairsplitting and simplification *) fun pair_induct_tac ctxt s rws i = - let val ss = Simplifier.local_simpset_of ctxt in + let val ss = simpset_of ctxt in res_inst_tac ctxt [(("x", 0), s)] @{thm Seq_induct} i THEN pair_tac ctxt "a" (i+3) THEN (REPEAT_DETERM (CHANGED (simp_tac ss (i+1)))) diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/Lift.thy --- a/src/HOLCF/Lift.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/Lift.thy Thu Jul 23 18:44:09 2009 +0200 @@ -61,7 +61,7 @@ method_setup defined = {* Scan.succeed (fn ctxt => SIMPLE_METHOD' - (etac @{thm lift_definedE} THEN' asm_simp_tac (local_simpset_of ctxt))) + (etac @{thm lift_definedE} THEN' asm_simp_tac (simpset_of ctxt))) *} "" lemma DefE: "Def x = \ \ R" diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/Tools/Domain/domain_theorems.ML --- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jul 23 18:44:09 2009 +0200 @@ -685,7 +685,7 @@ (* ----- theorems concerning finite approximation and finite induction ------ *) local - val iterate_Cprod_ss = simpset_of @{theory Fix}; + val iterate_Cprod_ss = global_simpset_of @{theory Fix}; val copy_con_rews = copy_rews @ con_rews; val copy_take_defs = (if n_eqs = 1 then [] else [ax_copy2_def]) @ axs_take_def; diff -r 253f6808dabe -r ef59550a55d3 src/HOLCF/Tools/fixrec.ML --- a/src/HOLCF/Tools/fixrec.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/HOLCF/Tools/fixrec.ML Thu Jul 23 18:44:09 2009 +0200 @@ -158,13 +158,13 @@ val thy = ProofContext.theory_of lthy; val names = map (Binding.name_of o fst o fst) fixes; val all_names = space_implode "_" names; - val (lhss,rhss) = ListPair.unzip (map (dest_eqs o snd) spec); + val (lhss, rhss) = ListPair.unzip (map (dest_eqs o snd) spec); val functional = lambda_tuple lhss (mk_tuple rhss); val fixpoint = mk_fix (mk_cabs functional); val cont_thm = Goal.prove lthy [] [] (mk_trp (mk_cont functional)) - (K (simp_tac (local_simpset_of lthy) 1)); + (K (simp_tac (simpset_of lthy) 1)); fun one_def (l as Free(n,_)) r = let val b = Long_Name.base_name n @@ -311,12 +311,12 @@ (*************************************************************************) (* proves a block of pattern matching equations as theorems, using unfold *) -fun make_simps lthy (unfold_thm, eqns : (Attrib.binding * term) list) = +fun make_simps ctxt (unfold_thm, eqns : (Attrib.binding * term) list) = let val tacs = [rtac (unfold_thm RS @{thm ssubst_lhs}) 1, - asm_simp_tac (local_simpset_of lthy) 1]; - fun prove_term t = Goal.prove lthy [] [] t (K (EVERY tacs)); + asm_simp_tac (simpset_of ctxt) 1]; + fun prove_term t = Goal.prove ctxt [] [] t (K (EVERY tacs)); fun prove_eqn (bind, eqn_t) = (bind, prove_term eqn_t); in map prove_eqn eqns @@ -399,7 +399,7 @@ fixrec_err "function is not declared as constant in theory"; val unfold_thm = PureThy.get_thm thy (cname^"_unfold"); val simp = Goal.prove_global thy [] [] eq - (fn _ => EVERY [stac unfold_thm 1, simp_tac (simpset_of thy) 1]); + (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]); in simp end; fun gen_add_fixpat prep_term prep_attrib ((name, srcs), strings) thy = diff -r 253f6808dabe -r ef59550a55d3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Thu Jul 23 18:44:09 2009 +0200 @@ -363,7 +363,7 @@ val print_simpset = Toplevel.unknown_context o Toplevel.keep (fn state => let val ctxt = Toplevel.context_of state - in Pretty.writeln (Simplifier.pretty_ss ctxt (Simplifier.local_simpset_of ctxt)) end); + in Pretty.writeln (Simplifier.pretty_ss ctxt (simpset_of ctxt)) end); val print_rules = Toplevel.unknown_context o Toplevel.keep (ContextRules.print_rules o Toplevel.context_of); diff -r 253f6808dabe -r ef59550a55d3 src/Pure/Tools/find_theorems.ML --- a/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Thu Jul 23 18:44:09 2009 +0200 @@ -207,7 +207,7 @@ fun filter_simp ctxt t (_, thm) = let - val mksimps = Simplifier.mksimps (Simplifier.local_simpset_of ctxt); + val mksimps = Simplifier.mksimps (simpset_of ctxt); val extract_simp = (map Thm.full_prop_of o mksimps, #1 o Logic.dest_equals o Logic.strip_imp_concl); val ss = is_matching_thm false extract_simp ctxt false t thm; diff -r 253f6808dabe -r ef59550a55d3 src/Tools/eqsubst.ML --- a/src/Tools/eqsubst.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/Tools/eqsubst.ML Thu Jul 23 18:44:09 2009 +0200 @@ -127,7 +127,7 @@ (* changes object "=" to meta "==" which prepares a given rewrite rule *) fun prep_meta_eq ctxt = - Simplifier.mksimps (Simplifier.local_simpset_of ctxt) #> map Drule.zero_var_indexes; + Simplifier.mksimps (simpset_of ctxt) #> map Drule.zero_var_indexes; (* a type abriviation for match information *) diff -r 253f6808dabe -r ef59550a55d3 src/ZF/IntDiv_ZF.thy --- a/src/ZF/IntDiv_ZF.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/ZF/IntDiv_ZF.thy Thu Jul 23 18:44:09 2009 +0200 @@ -1732,7 +1732,7 @@ (if ~b | #0 $<= integ_of w then integ_of v zdiv (integ_of w) else (integ_of v $+ #1) zdiv (integ_of w))" - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT) + apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) 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) done @@ -1778,7 +1778,7 @@ then #2 $* (integ_of v zmod integ_of w) $+ #1 else #2 $* ((integ_of v $+ #1) zmod integ_of w) - #1 else #2 $* (integ_of v zmod integ_of w))" - apply (simp_tac (simpset_of Int.thy add: zadd_assoc integ_of_BIT) + apply (simp_tac (global_simpset_of Int.thy add: zadd_assoc integ_of_BIT) 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) done diff -r 253f6808dabe -r ef59550a55d3 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/ZF/Tools/ind_cases.ML Thu Jul 23 18:44:09 2009 +0200 @@ -47,8 +47,7 @@ fun inductive_cases args thy = let - val read_prop = Syntax.read_prop (ProofContext.init thy); - val mk_cases = smart_cases thy (Simplifier.simpset_of thy) read_prop; + val mk_cases = smart_cases thy (global_simpset_of thy) (Syntax.read_prop_global thy); val facts = args |> map (fn ((name, srcs), props) => ((name, map (Attrib.attribute thy) srcs), map (Thm.no_attributes o single o mk_cases) props)); @@ -62,7 +61,7 @@ (Scan.lift (Scan.repeat1 Args.name_source) >> (fn props => fn ctxt => props - |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt) (Syntax.read_prop ctxt)) + |> map (smart_cases (ProofContext.theory_of ctxt) (simpset_of ctxt) (Syntax.read_prop ctxt)) |> Method.erule 0)) "dynamic case analysis on sets"; diff -r 253f6808dabe -r ef59550a55d3 src/ZF/UNITY/Constrains.thy --- a/src/ZF/UNITY/Constrains.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/ZF/UNITY/Constrains.thy Thu Jul 23 18:44:09 2009 +0200 @@ -471,7 +471,7 @@ (*proves "co" properties when the program is specified*) fun constrains_tac ctxt = - let val css as (cs, ss) = local_clasimpset_of ctxt in + let val css as (cs, ss) = clasimpset_of ctxt in SELECT_GOAL (EVERY [REPEAT (Always_Int_tac 1), REPEAT (etac @{thm Always_ConstrainsI} 1 @@ -494,7 +494,7 @@ (*For proving invariants*) fun always_tac ctxt i = - rtac @{thm AlwaysI} i THEN force_tac (local_clasimpset_of ctxt) i THEN constrains_tac ctxt i; + rtac @{thm AlwaysI} i THEN force_tac (clasimpset_of ctxt) i THEN constrains_tac ctxt i; *} setup Program_Defs.setup diff -r 253f6808dabe -r ef59550a55d3 src/ZF/UNITY/SubstAx.thy --- a/src/ZF/UNITY/SubstAx.thy Thu Jul 23 18:44:08 2009 +0200 +++ b/src/ZF/UNITY/SubstAx.thy Thu Jul 23 18:44:09 2009 +0200 @@ -351,7 +351,7 @@ ML {* (*proves "ensures/leadsTo" properties when the program is specified*) fun ensures_tac ctxt sact = - let val css as (cs, ss) = local_clasimpset_of ctxt in + let val css as (cs, ss) = clasimpset_of ctxt in SELECT_GOAL (EVERY [REPEAT (Always_Int_tac 1), etac @{thm Always_LeadsTo_Basis} 1 diff -r 253f6808dabe -r ef59550a55d3 src/ZF/int_arith.ML --- a/src/ZF/int_arith.ML Thu Jul 23 18:44:08 2009 +0200 +++ b/src/ZF/int_arith.ML Thu Jul 23 18:44:09 2009 +0200 @@ -145,7 +145,7 @@ val numeral_simp_ss = ZF_ss addsimps add_0s @ bin_simps @ tc_rules @ intifys fun numeral_simp_tac ss = ALLGOALS (simp_tac (Simplifier.inherit_context ss numeral_simp_ss)) - THEN ALLGOALS (asm_simp_tac (local_simpset_of (Simplifier.the_context ss))) + THEN ALLGOALS (asm_simp_tac (simpset_of (Simplifier.the_context ss))) val simplify_meta_eq = ArithData.simplify_meta_eq (add_0s @ mult_1s) end;