src/Provers/classical.ML
changeset 32148 253f6808dabe
parent 32091 30e2ffbba718
child 32261 05e687ddbcee
     1.1 --- a/src/Provers/classical.ML	Thu Jul 23 16:53:15 2009 +0200
     1.2 +++ b/src/Provers/classical.ML	Thu Jul 23 18:44:08 2009 +0200
     1.3 @@ -69,8 +69,8 @@
     1.4    val appSWrappers      : claset -> wrapper
     1.5    val appWrappers       : claset -> wrapper
     1.6  
     1.7 -  val claset_of: theory -> claset
     1.8 -  val local_claset_of   : Proof.context -> claset
     1.9 +  val global_claset_of  : theory -> claset
    1.10 +  val claset_of         : Proof.context -> claset
    1.11  
    1.12    val fast_tac          : claset -> int -> tactic
    1.13    val slow_tac          : claset -> int -> tactic
    1.14 @@ -852,7 +852,7 @@
    1.15  fun map_context_cs f = GlobalClaset.map (apsnd
    1.16    (fn ContextCS {swrappers, uwrappers} => make_context_cs (f (swrappers, uwrappers))));
    1.17  
    1.18 -fun claset_of thy =
    1.19 +fun global_claset_of thy =
    1.20    let val (cs, ctxt_cs) = GlobalClaset.get thy
    1.21    in context_cs (ProofContext.init thy) cs (ctxt_cs) end;
    1.22  
    1.23 @@ -874,13 +874,13 @@
    1.24    val init = get_claset;
    1.25  );
    1.26  
    1.27 -fun local_claset_of ctxt =
    1.28 +fun claset_of ctxt =
    1.29    context_cs ctxt (LocalClaset.get ctxt) (get_context_cs ctxt);
    1.30  
    1.31  
    1.32  (* generic clasets *)
    1.33  
    1.34 -val get_cs = Context.cases claset_of local_claset_of;
    1.35 +val get_cs = Context.cases global_claset_of claset_of;
    1.36  fun map_cs f = Context.mapping (map_claset f) (LocalClaset.map f);
    1.37  
    1.38  
    1.39 @@ -930,7 +930,7 @@
    1.40  fun some_rule_tac ctxt facts = SUBGOAL (fn (goal, i) =>
    1.41    let
    1.42      val [rules1, rules2, rules4] = ContextRules.find_rules false facts goal ctxt;
    1.43 -    val CS {xtra_netpair, ...} = local_claset_of ctxt;
    1.44 +    val CS {xtra_netpair, ...} = claset_of ctxt;
    1.45      val rules3 = ContextRules.find_rules_netpair true facts goal xtra_netpair;
    1.46      val rules = rules1 @ rules2 @ rules3 @ rules4;
    1.47      val ruleq = Drule.multi_resolves facts rules;
    1.48 @@ -969,10 +969,10 @@
    1.49    Args.del -- Args.colon >> K (I, rule_del)];
    1.50  
    1.51  fun cla_meth tac prems ctxt = METHOD (fn facts =>
    1.52 -  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (local_claset_of ctxt));
    1.53 +  ALLGOALS (Method.insert_tac (prems @ facts)) THEN tac (claset_of ctxt));
    1.54  
    1.55  fun cla_meth' tac prems ctxt = METHOD (fn facts =>
    1.56 -  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (local_claset_of ctxt)));
    1.57 +  HEADGOAL (Method.insert_tac (prems @ facts) THEN' tac (claset_of ctxt)));
    1.58  
    1.59  fun cla_method tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth tac);
    1.60  fun cla_method' tac = Args.bang_facts --| Method.sections cla_modifiers >> (cla_meth' tac);
    1.61 @@ -1014,6 +1014,6 @@
    1.62    OuterSyntax.improper_command "print_claset" "print context of Classical Reasoner"
    1.63      OuterKeyword.diag
    1.64      (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
    1.65 -      Toplevel.keep (print_cs o local_claset_of o Toplevel.context_of)));
    1.66 +      Toplevel.keep (print_cs o claset_of o Toplevel.context_of)));
    1.67  
    1.68  end;