# HG changeset patch
# User wenzelm
# Date 1248367448 -7200
# Node ID 253f6808dabe432cb5ad8eb1f7fa37742ed79d7f
# Parent  8228f67bfe182b72c1c77c815e2272b47876c6d6
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;

diff -r 8228f67bfe18 -r 253f6808dabe src/Provers/clasimp.ML
--- a/src/Provers/clasimp.ML	Thu Jul 23 16:53:15 2009 +0200
+++ b/src/Provers/clasimp.ML	Thu Jul 23 18:44:08 2009 +0200
@@ -26,7 +26,7 @@
   type clasimpset
   val get_css: Context.generic -> clasimpset
   val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
-  val local_clasimpset_of: Proof.context -> clasimpset
+  val clasimpset_of: Proof.context -> clasimpset
   val addSIs2: clasimpset * thm list -> clasimpset
   val addSEs2: clasimpset * thm list -> clasimpset
   val addSDs2: clasimpset * thm list -> clasimpset
@@ -73,8 +73,7 @@
   let val (cs', ss') = f (get_css context)
   in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
 
-fun local_clasimpset_of ctxt =
-  (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
+fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
 
 
 (* clasimpset operations *)
@@ -261,10 +260,10 @@
 (* methods *)
 
 fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
+  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt));
 
 fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
-  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
 
 
 fun clasimp_method tac =
diff -r 8228f67bfe18 -r 253f6808dabe src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Jul 23 16:53:15 2009 +0200
+++ b/src/Provers/classical.ML	Thu Jul 23 18:44:08 2009 +0200
@@ -69,8 +69,8 @@
   val appSWrappers      : claset -> wrapper
   val appWrappers       : claset -> wrapper
 
-  val claset_of: theory -> claset
-  val local_claset_of   : Proof.context -> claset
+  val global_claset_of  : theory -> claset
+  val claset_of         : Proof.context -> claset
 
   val fast_tac          : claset -> int -> tactic
   val slow_tac          : claset -> int -> tactic
@@ -852,7 +852,7 @@
 fun map_context_cs f = GlobalClaset.map (apsnd
   (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
 
-fun claset_of thy =
+fun global_claset_of thy =
   let val (cs, ctxt_cs) = GlobalClaset.get thy
   in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
 
@@ -874,13 +874,13 @@
   val init = get_claset;
 );
 
-fun local_claset_of ctxt =
+fun claset_of ctxt =
   context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
 
 
 (* generic clasets *)
 
-val get_cs = Context.cases claset_of local_claset_of;
+val get_cs = Context.cases global_claset_of claset_of;
 fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
 
 
@@ -930,7 +930,7 @@
 fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
   let
     val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
-    val CS {xtra_netpair, ...} = local_claset_of ctxt;
+    val CS {xtra_netpair, ...} = claset_of ctxt;
     val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
     val rules = rules1 @ rules2 @ rules3 @ rules4;
     val ruleq = Drule.multi_resolves facts rules;
@@ -969,10 +969,10 @@
   Args.del -- Args.colon >> K (I, rule_del)];
 
 fun cla_meth tac prems ctxt = METHOD (fn facts =>
-  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
+  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
 
 fun cla_meth' tac prems ctxt = METHOD (fn facts =>
-  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
+  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
 
 fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
 fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
@@ -1014,6 +1014,6 @@
   OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
     OuterKeyword.diag
     (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
-      Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of)));
+      Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
 
 end;
diff -r 8228f67bfe18 -r 253f6808dabe src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Thu Jul 23 16:53:15 2009 +0200
+++ b/src/Pure/simplifier.ML	Thu Jul 23 18:44:08 2009 +0200
@@ -9,10 +9,10 @@
 sig
   include BASIC_META_SIMPLIFIER
   val change_simpset: (simpset -> simpset) -> unit
-  val simpset_of: theory -> simpset
+  val global_simpset_of: theory -> simpset
   val Addsimprocs: simproc list -> unit
   val Delsimprocs: simproc list -> unit
-  val local_simpset_of: Proof.context -> simpset
+  val simpset_of: Proof.context -> simpset
   val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
   val safe_asm_full_simp_tac: simpset -> int -> tactic
   val               simp_tac: simpset -> int -> tactic
@@ -125,7 +125,8 @@
 
 fun map_simpset f = Context.theory_map (map_ss f);
 fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
-fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
+fun global_simpset_of thy =
+  MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
 
 fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
 fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
@@ -133,10 +134,10 @@
 
 (* local simpset *)
 
-fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
+fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
 
 val _ = ML_Antiquote.value "simpset"
-  (Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())");
+  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
 
 
 
@@ -331,7 +332,7 @@
 val simplified = conv_mode -- Attrib.thms >>
   (fn (f, ths) => Thm.rule_attribute (fn context =>
     f ((if null ths then I else MetaSimplifier.clear_ss)
-        (local_simpset_of (Context.proof_of context)) addsimps ths)));
+        (simpset_of (Context.proof_of context)) addsimps ths)));
 
 end;
 
@@ -390,12 +391,12 @@
   Method.setup (Binding.name simpN)
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       HEADGOAL (Method.insert_tac facts THEN'
-        (CHANGED_PROP oo tac) (local_simpset_of ctxt))))
+        (CHANGED_PROP oo tac) (simpset_of ctxt))))
     "simplification" #>
   Method.setup (Binding.name "simp_all")
     (simp_method more_mods (fn ctxt => fn tac => fn facts =>
       ALLGOALS (Method.insert_tac facts) THEN
-        (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)))
+        (CHANGED_PROP o ALLGOALS o tac) (simpset_of ctxt)))
     "simplification (all goals)";
 
 fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>