--- a/src/HOL/Auth/Message.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Auth/Message.thy Sun Jul 11 20:33:22 2004 +0200
@@ -932,21 +932,19 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_spy_analz_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ gen_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- atomic_spy_analz_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ atomic_spy_analz_tac (local_clasimpset_of ctxt) 1)) *}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1)) *}
+ Fake_insert_simp_tac (local_simpset_of ctxt) 1)) *}
"for debugging spy_analz"
--- a/src/HOL/Auth/Public.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Auth/Public.thy Sun Jul 11 20:33:22 2004 +0200
@@ -435,7 +435,7 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
+ gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
end
--- a/src/HOL/Auth/Shared.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Auth/Shared.thy Sun Jul 11 20:33:22 2004 +0200
@@ -272,7 +272,7 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
+ gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
lemma knows_subset_knows_Cons: "knows A evs <= knows A (e # evs)"
--- a/src/HOL/Hoare/Hoare.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Hoare/Hoare.thy Sun Jul 11 20:33:22 2004 +0200
@@ -235,7 +235,7 @@
method_setup vcg_simp = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
+ hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
"verification condition generator plus simplification"
end
--- a/src/HOL/Hoare/HoareAbort.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Hoare/HoareAbort.thy Sun Jul 11 20:33:22 2004 +0200
@@ -245,7 +245,7 @@
method_setup vcg_simp = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- hoare_tac (asm_full_simp_tac (Simplifier.get_local_simpset ctxt))1)) *}
+ hoare_tac (asm_full_simp_tac (local_simpset_of ctxt))1)) *}
"verification condition generator plus simplification"
(* Special syntax for guarded statements and guarded array updates: *)
--- a/src/HOL/Hyperreal/HyperDef.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy Sun Jul 11 20:33:22 2004 +0200
@@ -208,15 +208,13 @@
method_setup fuf = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- fuf_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ fuf_tac (local_clasimpset_of ctxt) 1)) *}
"free ultrafilter tactic"
method_setup ultra = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- ultra_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ ultra_tac (local_clasimpset_of ctxt) 1)) *}
"ultrafilter tactic"
--- a/src/HOL/SET-Protocol/MessageSET.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/SET-Protocol/MessageSET.thy Sun Jul 11 20:33:22 2004 +0200
@@ -936,21 +936,19 @@
method_setup spy_analz = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_spy_analz_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1))*}
+ gen_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
"for proving the Fake case when analz is involved"
method_setup atomic_spy_analz = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- atomic_spy_analz_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1))*}
+ atomic_spy_analz_tac (local_clasimpset_of ctxt) 1))*}
"for debugging spy_analz"
method_setup Fake_insert_simp = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- Fake_insert_simp_tac (Simplifier.get_local_simpset ctxt) 1))*}
+ Fake_insert_simp_tac (local_simpset_of ctxt) 1))*}
"for debugging spy_analz"
--- a/src/HOL/SET-Protocol/PublicSET.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/SET-Protocol/PublicSET.thy Sun Jul 11 20:33:22 2004 +0200
@@ -374,7 +374,7 @@
method_setup possibility = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_possibility_tac (Simplifier.get_local_simpset ctxt))) *}
+ gen_possibility_tac (local_simpset_of ctxt))) *}
"for proving possibility theorems"
--- a/src/HOL/Tools/inductive_package.ML Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Tools/inductive_package.ML Sun Jul 11 20:33:22 2004 +0200
@@ -600,7 +600,7 @@
fun mk_cases_meth (ctxt, raw_props) =
let
val thy = ProofContext.theory_of ctxt;
- val ss = Simplifier.get_local_simpset ctxt;
+ val ss = local_simpset_of ctxt;
val cprops = map (Thm.cterm_of (Theory.sign_of thy) o ProofContext.read_prop ctxt) raw_props;
in Method.erule 0 (map (smart_mk_cases thy ss) cprops) end;
--- a/src/HOL/Tools/meson.ML Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Tools/meson.ML Sun Jul 11 20:33:22 2004 +0200
@@ -419,7 +419,7 @@
fun meson_meth ctxt =
Method.SIMPLE_METHOD' HEADGOAL
- (CHANGED_PROP o meson_claset_tac (Classical.get_local_claset ctxt));
+ (CHANGED_PROP o meson_claset_tac (local_claset_of ctxt));
val skolemize_meth =
Method.SIMPLE_METHOD' HEADGOAL
--- a/src/HOL/Tools/recdef_package.ML Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/Tools/recdef_package.ML Sun Jul 11 20:33:22 2004 +0200
@@ -213,13 +213,15 @@
None => ctxt0
| Some src => Method.only_sectioned_args recdef_modifiers I src ctxt0);
val {simps, congs, wfs} = get_local_hints ctxt;
- val cs = Classical.get_local_claset ctxt;
- val ss = Simplifier.get_local_simpset ctxt addsimps simps;
+ val cs = local_claset_of ctxt;
+ val ss = local_simpset_of ctxt addsimps simps;
in (cs, ss, map #2 congs, wfs) end;
fun prepare_hints_i thy () =
- let val {simps, congs, wfs} = get_global_hints thy
- in (Classical.claset_of thy, Simplifier.simpset_of thy addsimps simps, map #2 congs, wfs) end;
+ 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, map #2 congs, wfs) end;
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy Sun Jul 11 20:33:22 2004 +0200
@@ -130,8 +130,7 @@
method_setup ns_induct = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- ns_induct_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ ns_induct_tac (local_clasimpset_of ctxt) 1)) *}
"for inductive reasoning about the Needham-Schroeder protocol"
text{*Converts invariants into statements about reachable states*}
--- a/src/HOL/UNITY/UNITY_Main.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy Sun Jul 11 20:33:22 2004 +0200
@@ -12,15 +12,13 @@
method_setup constrains = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_constrains_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
"for proving safety properties"
method_setup ensures_tac = {*
fn args => fn ctxt =>
Method.goal_args' (Scan.lift Args.name)
- (gen_ensures_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt))
+ (gen_ensures_tac (local_clasimpset_of ctxt))
args ctxt *}
"for proving progress properties"
--- a/src/Provers/clasimp.ML Fri Jul 09 16:33:20 2004 +0200
+++ b/src/Provers/clasimp.ML Sun Jul 11 20:33:22 2004 +0200
@@ -61,6 +61,7 @@
val change_global_css: (clasimpset * thm list -> clasimpset) -> theory attribute
val change_local_css: (clasimpset * thm list -> clasimpset) -> Proof.context attribute
val get_local_clasimpset: Proof.context -> clasimpset
+ val local_clasimpset_of: Proof.context -> clasimpset
val iff_add_global: theory attribute
val iff_add_global': theory attribute
val iff_del_global: theory attribute
@@ -276,6 +277,9 @@
fun get_local_clasimpset ctxt =
(Classical.get_local_claset ctxt, Simplifier.get_local_simpset ctxt);
+fun local_clasimpset_of ctxt =
+ (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
+
(* attributes *)
@@ -315,10 +319,10 @@
(* methods *)
fun clasimp_meth tac prems ctxt = Method.METHOD (fn facts =>
- ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (get_local_clasimpset ctxt));
+ ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
fun clasimp_meth' tac prems ctxt = Method.METHOD (fn facts =>
- HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (get_local_clasimpset ctxt)));
+ HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
val clasimp_method = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth;
val clasimp_method' = Method.bang_sectioned_args clasimp_modifiers o clasimp_meth';
--- a/src/ZF/Tools/ind_cases.ML Fri Jul 09 16:33:20 2004 +0200
+++ b/src/ZF/Tools/ind_cases.ML Sun Jul 11 20:33:22 2004 +0200
@@ -63,7 +63,7 @@
fun mk_cases_meth (ctxt, props) =
props
- |> map (smart_cases (ProofContext.theory_of ctxt) (Simplifier.get_local_simpset ctxt)
+ |> map (smart_cases (ProofContext.theory_of ctxt) (local_simpset_of ctxt)
(ProofContext.read_prop ctxt))
|> Method.erule 0;
--- a/src/ZF/UNITY/ClientImpl.thy Fri Jul 09 16:33:20 2004 +0200
+++ b/src/ZF/UNITY/ClientImpl.thy Sun Jul 11 20:33:22 2004 +0200
@@ -13,8 +13,7 @@
method_setup constrains = {*
Method.ctxt_args (fn ctxt =>
Method.METHOD (fn facts =>
- gen_constrains_tac (Classical.get_local_claset ctxt,
- Simplifier.get_local_simpset ctxt) 1)) *}
+ gen_constrains_tac (local_clasimpset_of ctxt) 1)) *}
"for proving safety properties"
consts