# HG changeset patch # User wenzelm # Date 1003170964 -7200 # Node ID aee100a086b10471d9e9dccc3bcc53ce823c3298 # Parent bdd2ac7c75ff2ba59ed80b265202f2dcb8fc5dc1 Tactic.orderlist; diff -r bdd2ac7c75ff -r aee100a086b1 src/Provers/blast.ML --- a/src/Provers/blast.ML Mon Oct 15 20:35:42 2001 +0200 +++ b/src/Provers/blast.ML Mon Oct 15 20:36:04 2001 +0200 @@ -565,13 +565,13 @@ val intrs = List.concat (map (fn (inet,_) => Net.unify_term inet pG) nps) - in map (fromIntrRule vars o #2) (orderlist intrs) end + in map (fromIntrRule vars o #2) (Tactic.orderlist intrs) end | _ => let val pP = mk_tprop (toTerm 3 P) val elims = List.concat (map (fn (_,enet) => Net.unify_term enet pP) nps) - in List.mapPartial (fromRule vars o #2) (orderlist elims) end; + in List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims) end; (*Pending formulae carry md (may duplicate) flags*) diff -r bdd2ac7c75ff -r aee100a086b1 src/Provers/classical.ML --- a/src/Provers/classical.ML Mon Oct 15 20:35:42 2001 +0200 +++ b/src/Provers/classical.ML Mon Oct 15 20:36:04 2001 +0200 @@ -780,7 +780,7 @@ (*version of bimatch_from_nets_tac that only applies rules that create precisely n subgoals.*) fun n_bimatch_from_nets_tac n = - biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true; + biresolution_from_nets_tac (Tactic.orderlist o filter (nsubgoalsP n)) true; fun eq_contr_tac i = ematch_tac [not_elim] i THEN eq_assume_tac i; val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;