adapted to new sort function;
authorwenzelm
Fri Dec 19 10:33:24 1997 +0100 (1997-12-19)
changeset 4452b2ee34200dab
parent 4451 f9e3e9f1af61
child 4453 bcb28bb925c1
adapted to new sort function;
src/Provers/Arith/cancel_factor.ML
src/Provers/Arith/cancel_sums.ML
src/Provers/ind.ML
     1.1 --- a/src/Provers/Arith/cancel_factor.ML	Fri Dec 19 10:31:13 1997 +0100
     1.2 +++ b/src/Provers/Arith/cancel_factor.ML	Fri Dec 19 10:33:24 1997 +0100
     1.3 @@ -43,7 +43,7 @@
     1.4        if t aconv u then (u, k + 1) :: uks
     1.5        else (t, 1) :: (u, k) :: uks;
     1.6  
     1.7 -fun count_terms ts = foldr ins_term (sort Logic.termless ts, []);
     1.8 +fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
     1.9  
    1.10  
    1.11  (* divide sum *)
     2.1 --- a/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:31:13 1997 +0100
     2.2 +++ b/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:33:24 1997 +0100
     2.3 @@ -42,7 +42,7 @@
     2.4  fun cancel ts [] vs = (ts, [], vs)
     2.5    | cancel [] us vs = ([], us, vs)
     2.6    | cancel (t :: ts) (u :: us) vs =
     2.7 -      (case Logic.term_ord (t, u) of
     2.8 +      (case Term.term_ord (t, u) of
     2.9          EQUAL => cancel ts us (t :: vs)
    2.10        | LESS => cons1 t (cancel ts (u :: us) vs)
    2.11        | GREATER => cons2 u (cancel (t :: ts) us vs));
    2.12 @@ -63,7 +63,7 @@
    2.13      None => None
    2.14    | Some bal =>
    2.15        let
    2.16 -        val (ts, us) = pairself (sort Logic.termless o Data.dest_sum) bal;
    2.17 +        val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
    2.18          val (ts', us', vs) = cancel ts us [];
    2.19        in
    2.20          if null vs then None
     3.1 --- a/src/Provers/ind.ML	Fri Dec 19 10:31:13 1997 +0100
     3.2 +++ b/src/Provers/ind.ML	Fri Dec 19 10:33:24 1997 +0100
     3.3 @@ -43,7 +43,7 @@
     3.4  fun all_frees_tac (var:string) i thm = 
     3.5      let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
     3.6          val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
     3.7 -        val frees' = sort(op>)(frees \ var) @ [var]
     3.8 +        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
     3.9      in foldl (qnt_tac i) (all_tac,frees') thm end;
    3.10  
    3.11  fun REPEAT_SIMP_TAC simp_tac n i =