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