# HG changeset patch
# User wenzelm
# Date 1089570802 -7200
# Node ID 02aed07e01bf323406f58dd7a05090e242638cb0
# Parent  726dc9146bb1e7fae61a25c7ddb0f6f990b3e7b2
local_cla/simpset_of;

diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Auth/Message.thy
--- 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"
 
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Auth/Public.thy
--- 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
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Auth/Shared.thy
--- 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)"
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Hoare/Hoare.thy
--- 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
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Hoare/HoareAbort.thy
--- 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: *)
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Hyperreal/HyperDef.thy
--- 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"
 
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/SET-Protocol/MessageSET.thy
--- 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"
 
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/SET-Protocol/PublicSET.thy
--- 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"
 
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Tools/inductive_package.ML
--- 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;
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Tools/meson.ML
--- 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
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/Tools/recdef_package.ML
--- 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;
 
 
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/UNITY/Simple/NSP_Bad.thy
--- 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*}
diff -r 726dc9146bb1 -r 02aed07e01bf src/HOL/UNITY/UNITY_Main.thy
--- 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"
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/Provers/clasimp.ML
--- 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';
diff -r 726dc9146bb1 -r 02aed07e01bf src/ZF/Tools/ind_cases.ML
--- 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;
 
diff -r 726dc9146bb1 -r 02aed07e01bf src/ZF/UNITY/ClientImpl.thy
--- 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