added Int.int;

--- a/src/Pure/basis.ML	Tue Oct 13 14:24:35 1998 +0200
+++ b/src/Pure/basis.ML	Tue Oct 13 14:25:01 1998 +0200
@@ -36,6 +36,7 @@
 
 structure Int =
   struct
+  type int = int
   fun toString (i: int) = makestring i;
   fun max (x, y) = if x < y then y else x : int;
   fun min (x, y) = if x < y then x else y : int;