adapted to new term order;
authorwenzelm
Tue Dec 02 12:42:59 1997 +0100 (1997-12-02)
changeset 434615fab62268c3
parent 4345 7e9436ffb813
child 4347 d683b7898c61
adapted to new term order;
src/Provers/Arith/cancel_sums.ML
     1.1 --- a/src/Provers/Arith/cancel_sums.ML	Tue Dec 02 12:42:28 1997 +0100
     1.2 +++ b/src/Provers/Arith/cancel_sums.ML	Tue Dec 02 12:42:59 1997 +0100
     1.3 @@ -38,15 +38,12 @@
     1.4  fun cons2 y (x, ys, z) = (x, y :: ys, z);
     1.5  fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
     1.6  
     1.7 -(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.termord*)
     1.8 +(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*)
     1.9  fun cancel ts [] vs = (ts, [], vs)
    1.10    | cancel [] us vs = ([], us, vs)
    1.11    | cancel (t :: ts) (u :: us) vs =
    1.12 -      (case Logic.termord (t, u) of
    1.13 -        EQUAL =>
    1.14 -          if t aconv u then cancel ts us (t :: vs)
    1.15 -          else cons12 t u (cancel ts us vs)
    1.16 -            (*potential incompleteness! -- termord not strictly antisymmetric*)
    1.17 +      (case Logic.term_ord (t, u) of
    1.18 +        EQUAL => cancel ts us (t :: vs)
    1.19        | LESS => cons1 t (cancel ts (u :: us) vs)
    1.20        | GREATER => cons2 u (cancel (t :: ts) us vs));
    1.21