src/Provers/classical.ML
changeset 11783 aee100a086b1
parent 11754 3928d990c22f
child 12053 7e2e84e503ce
--- 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;