src/Provers/classical.ML
changeset 33317 b4534348b8fd
parent 32960 69916a850301
child 33339 d41f77196338
     1.1 --- a/src/Provers/classical.ML	Thu Oct 29 16:59:12 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Thu Oct 29 17:58:26 2009 +0100
     1.3 @@ -670,7 +670,7 @@
     1.4  (*version of bimatch_from_nets_tac that only applies rules that
     1.5    create precisely n subgoals.*)
     1.6  fun n_bimatch_from_nets_tac n =
     1.7 -    biresolution_from_nets_tac (order_list o List.filter (nsubgoalsP n)) true;
     1.8 +    biresolution_from_nets_tac (order_list o filter (nsubgoalsP n)) true;
     1.9  
    1.10  fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
    1.11  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;