src/Provers/classical.ML
changeset 30558 2ef9892114fd
parent 30541 9f168bdc468a
child 30609 983e8b6e4e69
     1.1 --- a/src/Provers/classical.ML	Tue Mar 17 13:33:21 2009 +0100
     1.2 +++ b/src/Provers/classical.ML	Tue Mar 17 14:09:20 2009 +0100
     1.3 @@ -688,7 +688,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 (Tactic.orderlist o List.filter (nsubgoalsP n)) true;
     1.8 +    biresolution_from_nets_tac (order_list o List.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;