# HG changeset patch
# User wenzelm
# Date 908281501 -7200
# Node ID 983ce142121178f740d71bfc9f290d00927bce85
# Parent  1b3e48bdbb931d7de68bd34d0b799936d1003c1f
added Int.int;

diff -r 1b3e48bdbb93 -r 983ce1421211 src/Pure/basis.ML
--- 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;