Tactic.orderlist;
authorwenzelm
Mon Oct 15 20:36:04 2001 +0200 (2001-10-15)
changeset 11783aee100a086b1
parent 11782 bdd2ac7c75ff
child 11784 b66b198ee29a
Tactic.orderlist;
src/Provers/blast.ML
src/Provers/classical.ML
     1.1 --- a/src/Provers/blast.ML	Mon Oct 15 20:35:42 2001 +0200
     1.2 +++ b/src/Provers/blast.ML	Mon Oct 15 20:36:04 2001 +0200
     1.3 @@ -565,13 +565,13 @@
     1.4  	    val intrs = List.concat 
     1.5  		             (map (fn (inet,_) => Net.unify_term inet pG) 
     1.6  			      nps)
     1.7 -	in  map (fromIntrRule vars o #2) (orderlist intrs)  end
     1.8 +	in  map (fromIntrRule vars o #2) (Tactic.orderlist intrs)  end
     1.9      | _ =>
    1.10  	let val pP = mk_tprop (toTerm 3 P)
    1.11  	    val elims = List.concat 
    1.12  		             (map (fn (_,enet) => Net.unify_term enet pP) 
    1.13  			      nps)
    1.14 -	in  List.mapPartial (fromRule vars o #2) (orderlist elims)  end;
    1.15 +	in  List.mapPartial (fromRule vars o #2) (Tactic.orderlist elims)  end;
    1.16  
    1.17  
    1.18  (*Pending formulae carry md (may duplicate) flags*)
     2.1 --- a/src/Provers/classical.ML	Mon Oct 15 20:35:42 2001 +0200
     2.2 +++ b/src/Provers/classical.ML	Mon Oct 15 20:36:04 2001 +0200
     2.3 @@ -780,7 +780,7 @@
     2.4  (*version of bimatch_from_nets_tac that only applies rules that
     2.5    create precisely n subgoals.*)
     2.6  fun n_bimatch_from_nets_tac n =
     2.7 -    biresolution_from_nets_tac (orderlist o filter (nsubgoalsP n)) true;
     2.8 +    biresolution_from_nets_tac (Tactic.orderlist o filter (nsubgoalsP n)) true;
     2.9  
    2.10  fun eq_contr_tac i = ematch_tac [not_elim] i  THEN  eq_assume_tac i;
    2.11  val eq_assume_contr_tac = eq_assume_tac ORELSE' eq_contr_tac;