--- 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;