--- 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