# HG changeset patch
# User wenzelm
# Date 882524004 -3600
# Node ID b2ee34200dab4396fae0bae0e0728e496fc19f03
# Parent  f9e3e9f1af612bd184bbdf7337c05bcca521c3b1
adapted to new sort function;

diff -r f9e3e9f1af61 -r b2ee34200dab src/Provers/Arith/cancel_factor.ML
--- a/src/Provers/Arith/cancel_factor.ML	Fri Dec 19 10:31:13 1997 +0100
+++ b/src/Provers/Arith/cancel_factor.ML	Fri Dec 19 10:33:24 1997 +0100
@@ -43,7 +43,7 @@
       if t aconv u then (u, k + 1) :: uks
       else (t, 1) :: (u, k) :: uks;
 
-fun count_terms ts = foldr ins_term (sort Logic.termless ts, []);
+fun count_terms ts = foldr ins_term (sort Term.term_ord ts, []);
 
 
 (* divide sum *)
diff -r f9e3e9f1af61 -r b2ee34200dab src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:31:13 1997 +0100
+++ b/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:33:24 1997 +0100
@@ -42,7 +42,7 @@
 fun cancel ts [] vs = (ts, [], vs)
   | cancel [] us vs = ([], us, vs)
   | cancel (t :: ts) (u :: us) vs =
-      (case Logic.term_ord (t, u) of
+      (case Term.term_ord (t, u) of
         EQUAL => cancel ts us (t :: vs)
       | LESS => cons1 t (cancel ts (u :: us) vs)
       | GREATER => cons2 u (cancel (t :: ts) us vs));
@@ -63,7 +63,7 @@
     None => None
   | Some bal =>
       let
-        val (ts, us) = pairself (sort Logic.termless o Data.dest_sum) bal;
+        val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
         val (ts', us', vs) = cancel ts us [];
       in
         if null vs then None
diff -r f9e3e9f1af61 -r b2ee34200dab src/Provers/ind.ML
--- a/src/Provers/ind.ML	Fri Dec 19 10:31:13 1997 +0100
+++ b/src/Provers/ind.ML	Fri Dec 19 10:33:24 1997 +0100
@@ -43,7 +43,7 @@
 fun all_frees_tac (var:string) i thm = 
     let val tsig = #tsig(Sign.rep_sg(#sign(rep_thm thm)));
         val frees = add_term_frees tsig (nth_elem(i-1,prems_of thm),[var]);
-        val frees' = sort(op>)(frees \ var) @ [var]
+        val frees' = sort (rev_order o string_ord) (frees \ var) @ [var]
     in foldl (qnt_tac i) (all_tac,frees') thm end;
 
 fun REPEAT_SIMP_TAC simp_tac n i =