src/Provers/classical.ML
changeset 11723 2b4a0d630071
parent 11181 d04f57b91166
child 11754 3928d990c22f
     1.1 --- a/src/Provers/classical.ML	Thu Oct 11 21:25:45 2001 +0200
     1.2 +++ b/src/Provers/classical.ML	Fri Oct 12 12:05:02 2001 +0200
     1.3 @@ -75,7 +75,6 @@
     1.4    val addSE2            : claset * (string * thm) -> claset
     1.5    val appSWrappers      : claset -> wrapper
     1.6    val appWrappers       : claset -> wrapper
     1.7 -  val trace_rules       : bool ref
     1.8  
     1.9    val claset_ref_of_sg: Sign.sg -> claset ref
    1.10    val claset_ref_of: theory -> claset ref
    1.11 @@ -1070,11 +1069,10 @@
    1.12  (* get nets (appropriate order for semi-automatic methods) *)
    1.13  
    1.14  local
    1.15 -  val imp_elim_netpair = insert (0, 0) ([], [imp_elim]) empty_netpair;
    1.16    val not_elim_netpair = insert (0, 0) ([], [Data.not_elim]) empty_netpair;
    1.17  in
    1.18    fun get_nets (CS {safe0_netpair, safep_netpair, haz_netpair, dup_netpair, xtra_netpair, ...}) =
    1.19 -    [imp_elim_netpair, safe0_netpair, safep_netpair, not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair];
    1.20 +    [safe0_netpair, safep_netpair, not_elim_netpair, haz_netpair, dup_netpair, xtra_netpair];
    1.21  end;
    1.22  
    1.23  
    1.24 @@ -1084,22 +1082,10 @@
    1.25    Method.METHOD (HEADGOAL o tac ctxt (get_local_claset ctxt));
    1.26  
    1.27  
    1.28 -val trace_rules = ref false;
    1.29 -
    1.30  local
    1.31  
    1.32 -fun trace rules i =
    1.33 -  if not (! trace_rules) then ()
    1.34 -  else Pretty.writeln (Pretty.big_list ("trying standard rule(s) on goal #" ^ string_of_int i ^ ":")
    1.35 -    (map Display.pretty_thm rules));
    1.36 -
    1.37 -
    1.38  fun order_rules xs = map snd (Tactic.orderlist (map (apfst recover_order) xs));
    1.39  
    1.40 -fun find_rules concl nets =
    1.41 -  let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl)
    1.42 -  in flat (map rules_of nets) end;
    1.43 -
    1.44  fun find_erules [] _ = []
    1.45    | find_erules (fact :: _) nets =
    1.46        let
    1.47 @@ -1107,6 +1093,10 @@
    1.48          fun erules_of (_, enet) = order_rules (may_unify enet fact);
    1.49        in flat (map erules_of nets) end;
    1.50  
    1.51 +fun find_rules concl nets =
    1.52 +  let fun rules_of (inet, _) = order_rules (Net.unify_term inet concl)
    1.53 +  in flat (map rules_of nets) end;
    1.54 +
    1.55  fun some_rule_tac cs facts =
    1.56    let
    1.57      val nets = get_nets cs;
    1.58 @@ -1117,11 +1107,11 @@
    1.59          val irules = find_rules (Logic.strip_assums_concl goal) nets;
    1.60          val rules = erules @ irules;
    1.61          val ruleq = Method.multi_resolves facts rules;
    1.62 -      in trace rules i; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
    1.63 +      in Method.trace rules; fn st => Seq.flat (Seq.map (fn rule => Tactic.rtac rule i st) ruleq) end);
    1.64    in tac end;
    1.65  
    1.66  fun rule_tac [] ctxt cs facts =
    1.67 -    some_rule_tac cs facts ORELSE' Method.some_rule_tac [] ctxt facts
    1.68 +    Method.some_rule_tac [] ctxt facts APPEND' some_rule_tac cs facts
    1.69    | rule_tac rules _ _ facts = Method.rule_tac rules facts;
    1.70  
    1.71  fun default_tac rules ctxt cs facts =