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:08 2009 +0200 (2009-07-23)
changeset 32148253f6808dabe
parent 32147 8228f67bfe18
child 32149 ef59550a55d3
renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
src/Provers/clasimp.ML
src/Provers/classical.ML
src/Pure/simplifier.ML
     1.1 --- a/src/Provers/clasimp.ML	Thu Jul 23 16:53:15 2009 +0200
     1.2 +++ b/src/Provers/clasimp.ML	Thu Jul 23 18:44:08 2009 +0200
     1.3 @@ -26,7 +26,7 @@
     1.4    type clasimpset
     1.5    val get_css: Context.generic -> clasimpset
     1.6    val map_css: (clasimpset -> clasimpset) -> Context.generic -> Context.generic
     1.7 -  val local_clasimpset_of: Proof.context -> clasimpset
     1.8 +  val clasimpset_of: Proof.context -> clasimpset
     1.9    val addSIs2: clasimpset * thm list -> clasimpset
    1.10    val addSEs2: clasimpset * thm list -> clasimpset
    1.11    val addSDs2: clasimpset * thm list -> clasimpset
    1.12 @@ -73,8 +73,7 @@
    1.13    let val (cs', ss') = f (get_css context)
    1.14    in context |> Classical.map_cs (K cs') |> Simplifier.map_ss (K ss') end;
    1.15  
    1.16 -fun local_clasimpset_of ctxt =
    1.17 -  (Classical.local_claset_of ctxt, Simplifier.local_simpset_of ctxt);
    1.18 +fun clasimpset_of ctxt = (Classical.claset_of ctxt, Simplifier.simpset_of ctxt);
    1.19  
    1.20  
    1.21  (* clasimpset operations *)
    1.22 @@ -261,10 +260,10 @@
    1.23  (* methods *)
    1.24  
    1.25  fun clasimp_meth tac prems ctxt = METHOD (fn facts =>
    1.26 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_clasimpset_of ctxt));
    1.27 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (clasimpset_of ctxt));
    1.28  
    1.29  fun clasimp_meth' tac prems ctxt = METHOD (fn facts =>
    1.30 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_clasimpset_of ctxt)));
    1.31 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (clasimpset_of ctxt)));
    1.32  
    1.33  
    1.34  fun clasimp_method tac =
     2.1 --- a/src/Provers/classical.ML	Thu Jul 23 16:53:15 2009 +0200
     2.2 +++ b/src/Provers/classical.ML	Thu Jul 23 18:44:08 2009 +0200
     2.3 @@ -69,8 +69,8 @@
     2.4    val appSWrappers      : claset -> wrapper
     2.5    val appWrappers       : claset -> wrapper
     2.6  
     2.7 -  val claset_of: theory -> claset
     2.8 -  val local_claset_of   : Proof.context -> claset
     2.9 +  val global_claset_of  : theory -> claset
    2.10 +  val claset_of         : Proof.context -> claset
    2.11  
    2.12    val fast_tac          : claset -> int -> tactic
    2.13    val slow_tac          : claset -> int -> tactic
    2.14 @@ -852,7 +852,7 @@
    2.15  fun map_context_cs f = GlobalClaset.map (apsnd
    2.16    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    2.17  
    2.18 -fun claset_of thy =
    2.19 +fun global_claset_of thy =
    2.20    let val (cs, ctxt_cs) = GlobalClaset.get thy
    2.21    in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
    2.22  
    2.23 @@ -874,13 +874,13 @@
    2.24    val init = get_claset;
    2.25  );
    2.26  
    2.27 -fun local_claset_of ctxt =
    2.28 +fun claset_of ctxt =
    2.29    context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
    2.30  
    2.31  
    2.32  (* generic clasets *)
    2.33  
    2.34 -val get_cs = Context.cases claset_of local_claset_of;
    2.35 +val get_cs = Context.cases global_claset_of claset_of;
    2.36  fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
    2.37  
    2.38  
    2.39 @@ -930,7 +930,7 @@
    2.40  fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
    2.41    let
    2.42      val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
    2.43 -    val CS {xtra_netpair, ...} = local_claset_of ctxt;
    2.44 +    val CS {xtra_netpair, ...} = claset_of ctxt;
    2.45      val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
    2.46      val rules = rules1 @ rules2 @ rules3 @ rules4;
    2.47      val ruleq = Drule.multi_resolves facts rules;
    2.48 @@ -969,10 +969,10 @@
    2.49    Args.del -- Args.colon >> K (I, rule_del)];
    2.50  
    2.51  fun cla_meth tac prems ctxt = METHOD (fn facts =>
    2.52 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
    2.53 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
    2.54  
    2.55  fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    2.56 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
    2.57 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
    2.58  
    2.59  fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    2.60  fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    2.61 @@ -1014,6 +1014,6 @@
    2.62    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    2.63      OuterKeyword.diag
    2.64      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    2.65 -      Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of)));
    2.66 +      Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
    2.67  
    2.68  end;
     3.1 --- a/src/Pure/simplifier.ML	Thu Jul 23 16:53:15 2009 +0200
     3.2 +++ b/src/Pure/simplifier.ML	Thu Jul 23 18:44:08 2009 +0200
     3.3 @@ -9,10 +9,10 @@
     3.4  sig
     3.5    include BASIC_META_SIMPLIFIER
     3.6    val change_simpset: (simpset -> simpset) -> unit
     3.7 -  val simpset_of: theory -> simpset
     3.8 +  val global_simpset_of: theory -> simpset
     3.9    val Addsimprocs: simproc list -> unit
    3.10    val Delsimprocs: simproc list -> unit
    3.11 -  val local_simpset_of: Proof.context -> simpset
    3.12 +  val simpset_of: Proof.context -> simpset
    3.13    val generic_simp_tac: bool -> bool * bool * bool -> simpset -> int -> tactic
    3.14    val safe_asm_full_simp_tac: simpset -> int -> tactic
    3.15    val               simp_tac: simpset -> int -> tactic
    3.16 @@ -125,7 +125,8 @@
    3.17  
    3.18  fun map_simpset f = Context.theory_map (map_ss f);
    3.19  fun change_simpset f = Context.>> (Context.map_theory (map_simpset f));
    3.20 -fun simpset_of thy = MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
    3.21 +fun global_simpset_of thy =
    3.22 +  MetaSimplifier.context (ProofContext.init thy) (get_ss (Context.Theory thy));
    3.23  
    3.24  fun Addsimprocs args = change_simpset (fn ss => ss addsimprocs args);
    3.25  fun Delsimprocs args = change_simpset (fn ss => ss delsimprocs args);
    3.26 @@ -133,10 +134,10 @@
    3.27  
    3.28  (* local simpset *)
    3.29  
    3.30 -fun local_simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
    3.31 +fun simpset_of ctxt = MetaSimplifier.context ctxt (get_ss (Context.Proof ctxt));
    3.32  
    3.33  val _ = ML_Antiquote.value "simpset"
    3.34 -  (Scan.succeed "Simplifier.local_simpset_of (ML_Context.the_local_context ())");
    3.35 +  (Scan.succeed "Simplifier.simpset_of (ML_Context.the_local_context ())");
    3.36  
    3.37  
    3.38  
    3.39 @@ -331,7 +332,7 @@
    3.40  val simplified = conv_mode -- Attrib.thms >>
    3.41    (fn (f, ths) => Thm.rule_attribute (fn context =>
    3.42      f ((if null ths then I else MetaSimplifier.clear_ss)
    3.43 -        (local_simpset_of (Context.proof_of context)) addsimps ths)));
    3.44 +        (simpset_of (Context.proof_of context)) addsimps ths)));
    3.45  
    3.46  end;
    3.47  
    3.48 @@ -390,12 +391,12 @@
    3.49    Method.setup (Binding.name simpN)
    3.50      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
    3.51        HEADGOAL (Method.insert_tac facts THEN'
    3.52 -        (CHANGED_PROP oo tac) (local_simpset_of ctxt))))
    3.53 +        (CHANGED_PROP oo tac) (simpset_of ctxt))))
    3.54      "simplification" #>
    3.55    Method.setup (Binding.name "simp_all")
    3.56      (simp_method more_mods (fn ctxt => fn tac => fn facts =>
    3.57        ALLGOALS (Method.insert_tac facts) THEN
    3.58 -        (CHANGED_PROP o ALLGOALS o tac) (local_simpset_of ctxt)))
    3.59 +        (CHANGED_PROP o ALLGOALS o tac) (simpset_of ctxt)))
    3.60      "simplification (all goals)";
    3.61  
    3.62  fun easy_setup reflect trivs = method_setup [] #> Context.theory_map (map_ss (fn _ =>