# HG changeset patch
# User wenzelm
# Date 881062979 -3600
# Node ID 15fab62268c32fd18025aafe6793450bbd0ddc73
# Parent  7e9436ffb813112e7f6330f99e7f902c1819b3df
adapted to new term order;

diff -r 7e9436ffb813 -r 15fab62268c3 src/Provers/Arith/cancel_sums.ML
--- a/src/Provers/Arith/cancel_sums.ML	Tue Dec 02 12:42:28 1997 +0100
+++ b/src/Provers/Arith/cancel_sums.ML	Tue Dec 02 12:42:59 1997 +0100
@@ -38,15 +38,12 @@
 fun cons2 y (x, ys, z) = (x, y :: ys, z);
 fun cons12 x y (xs, ys, z) = (x :: xs, y :: ys, z);
 
-(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.termord*)
+(*symmetric difference of multisets -- assumed to be sorted wrt. Logic.term_ord*)
 fun cancel ts [] vs = (ts, [], vs)
   | cancel [] us vs = ([], us, vs)
   | cancel (t :: ts) (u :: us) vs =
-      (case Logic.termord (t, u) of
-        EQUAL =>
-          if t aconv u then cancel ts us (t :: vs)
-          else cons12 t u (cancel ts us vs)
-            (*potential incompleteness! -- termord not strictly antisymmetric*)
+      (case Logic.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));