src/Provers/Arith/cancel_sums.ML
changeset 4452 b2ee34200dab
parent 4346 15fab62268c3
child 15027 d23887300b96
     1.1 --- a/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:31:13 1997 +0100
     1.2 +++ b/src/Provers/Arith/cancel_sums.ML	Fri Dec 19 10:33:24 1997 +0100
     1.3 @@ -42,7 +42,7 @@
     1.4  fun cancel ts [] vs = (ts, [], vs)
     1.5    | cancel [] us vs = ([], us, vs)
     1.6    | cancel (t :: ts) (u :: us) vs =
     1.7 -      (case Logic.term_ord (t, u) of
     1.8 +      (case Term.term_ord (t, u) of
     1.9          EQUAL => cancel ts us (t :: vs)
    1.10        | LESS => cons1 t (cancel ts (u :: us) vs)
    1.11        | GREATER => cons2 u (cancel (t :: ts) us vs));
    1.12 @@ -63,7 +63,7 @@
    1.13      None => None
    1.14    | Some bal =>
    1.15        let
    1.16 -        val (ts, us) = pairself (sort Logic.termless o Data.dest_sum) bal;
    1.17 +        val (ts, us) = pairself (sort Term.term_ord o Data.dest_sum) bal;
    1.18          val (ts', us', vs) = cancel ts us [];
    1.19        in
    1.20          if null vs then None