Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2003-11-02 18:34:53 -0800 (Sun, 02 Nov 2003)
Revision: 5066
Log message:

      Fixed the second ingredient of the difference in behavior with Term_ds and Term_std:
      One place in arith.ml was still using simple equality to compare terms. Because of it arith.ml produced result that revealed some imperfect logic in itt_int_arith (was fixed yesterday).
      I think this commit closes the issue completely.
      

Changes	Path
+50 -36	metaprl/refiner/reflib/arith.ml
+1 -2	metaprl/theories/itt/itt_int_arith.ml
+1 -0	metaprl/theories/itt/itt_int_arith.mli