tuned method "rule" and "default";
authorwenzelm
Sat Nov 04 18:44:34 2000 +0100 (2000-11-04 ago)
changeset 10394eef9e422929a
parent 10393 b2a212304fb4
child 10395 7ef380745743
tuned method "rule" and "default";
src/Provers/classical.ML
     1.1 --- a/src/Provers/classical.ML	Sat Nov 04 18:42:29 2000 +0100
     1.2 +++ b/src/Provers/classical.ML	Sat Nov 04 18:44:34 2000 +0100
     1.3 @@ -1079,7 +1079,7 @@
     1.4  (* METHOD_CLASET' *)
     1.5  
     1.6  fun METHOD_CLASET' tac ctxt =
     1.7 -  Method.METHOD (HEADGOAL o tac (get_local_claset ctxt));
     1.8 +  Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
     1.9  
    1.10  
    1.11  val trace_rules = ref false;
    1.12 @@ -1105,7 +1105,6 @@
    1.13          fun erules_of (_, enet) = order_rules (may_unify enet fact);
    1.14        in flat (map erules_of nets) end;
    1.15  
    1.16 -
    1.17  fun some_rule_tac cs facts =
    1.18    let
    1.19      val nets = get_nets cs;
    1.20 @@ -1119,17 +1118,17 @@
    1.21        in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
    1.22    in tac end;
    1.23  
    1.24 -fun rule_tac [] cs facts = some_rule_tac cs facts
    1.25 -  | rule_tac rules _ facts = Method.rule_tac rules facts;
    1.26 +fun rule_tac [] ctxt cs facts =
    1.27 +    some_rule_tac cs facts ORELSE' Method.some_rule_tac [] ctxt facts
    1.28 +  | rule_tac rules _ _ facts = Method.rule_tac rules facts;
    1.29  
    1.30  fun default_tac rules ctxt cs facts =
    1.31 -  rule_tac rules cs facts ORELSE'
    1.32 -  Method.some_rule_tac rules ctxt facts ORELSE'
    1.33 +  rule_tac rules ctxt cs facts ORELSE'
    1.34    AxClass.default_intro_classes_tac facts;
    1.35  
    1.36  in
    1.37    val rule = METHOD_CLASET' o rule_tac;
    1.38 -  fun default rules ctxt = METHOD_CLASET' (default_tac rules ctxt) ctxt;
    1.39 +  val default = METHOD_CLASET' o default_tac;
    1.40  end;
    1.41  
    1.42  
    1.43 @@ -1137,7 +1136,7 @@
    1.44  
    1.45  local
    1.46  
    1.47 -fun intro_elim_tac netpair_of res_tac rules cs facts =
    1.48 +fun intro_elim_tac netpair_of res_tac rules _ cs facts =
    1.49    let
    1.50      val tac =
    1.51        if null rules then FIRST' (map (bimatch_from_nets_tac o netpair_of) (get_nets cs))