--- a/src/Provers/classical.ML Thu Oct 29 16:59:12 2009 +0100
+++ b/src/Provers/classical.ML Thu Oct 29 17:58:26 2009 +0100
@@ -670,7 +670,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 (order_list o List.filter (nsubgoalsP n)) true;
+ biresolution_from_nets_tac (order_list 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;