src/Pure/basis.ML
changeset 5643 983ce1421211
parent 5208 cea0adbc7276
child 5836 90f7d9f1a0cc
     1.1 --- a/src/Pure/basis.ML	Tue Oct 13 14:24:35 1998 +0200
     1.2 +++ b/src/Pure/basis.ML	Tue Oct 13 14:25:01 1998 +0200
     1.3 @@ -36,6 +36,7 @@
     1.4  
     1.5  structure Int =
     1.6    struct
     1.7 +  type int = int
     1.8    fun toString (i: int) = makestring i;
     1.9    fun max (x, y) = if x < y then y else x : int;
    1.10    fun min (x, y) = if x < y then x else y : int;