src/Tools/integer.ML

 Unbounded integers.
 *)
 
 signature INTEGER =
 sig
-  type int
+  eqtype int
   val zero: int
   val one: int
   val two: int
   val int: Int.int -> int
   val machine_int: int -> Int.int

 end;
 
 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;
 fun a <=% b = Integer.le a b;
 fun a >% b = b <% a;
 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*)