--- 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*)
--- 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;