# HG changeset patch
# User wenzelm
# Date 1181341727 -7200
# Node ID 404988d8b1e0b5bb57850b34112ef2050c92493e
# Parent  06f108974fa180b3da14fbcbd67f8c8a5e6ba009
eqtype int -- explicitly encourage overloaded equality;
tuned -%;
removed obsolete Intt;

diff -r 06f108974fa1 -r 404988d8b1e0 src/Tools/integer.ML
--- a/src/Tools/integer.ML	Sat Jun 09 00:28:46 2007 +0200
+++ b/src/Tools/integer.ML	Sat Jun 09 00:28:47 2007 +0200
@@ -7,7 +7,7 @@
 
 signature INTEGER =
 sig
-  type int
+  eqtype int
   val zero: int
   val one: int
   val two: int
@@ -98,11 +98,11 @@
 type integer = Integer.int;
 
 infix 7 *%;
-infix 6 +% -%; 
+infix 6 +% -%;
 infix 4 =% <% <=% >% >=% <>%;
 
 fun a +% b = Integer.add a b;
-fun a -% b = a +% Integer.neg b;
+fun a -% b = Integer.sub a b;
 fun a *% b = Integer.mult a b;
 fun a =% b = Integer.eq (a, b);
 fun a <% b = Integer.lt a b;
@@ -111,6 +111,5 @@
 fun a >=% b = b <=% a;
 fun a <>% b = not (a =% b);
 
-structure Intt = Integer; (*FIXME*)
 val gcd = uncurry Integer.gcd; (*FIXME*)
 val lcm = uncurry Integer.lcm; (*FIXME*)