# HG changeset patch
# User wenzelm
# Date 1210756656 -7200
# Node ID 0ae304689d018c561a4f5d99f57d07553a744a86
# Parent  d43264d547f85387e746320ff9acd5b4a9d158ec
explicit constraints for int literals;

diff -r d43264d547f8 -r 0ae304689d01 src/Pure/General/seq.ML
--- a/src/Pure/General/seq.ML	Wed May 14 11:16:11 2008 +0200
+++ b/src/Pure/General/seq.ML	Wed May 14 11:17:36 2008 +0200
@@ -89,7 +89,7 @@
 (*the list of the first n elements, paired with rest of sequence;
   if length of list is less than n, then sequence had less than n elements*)
 fun chop n xq =
-  if n <= 0 then ([], xq)
+  if n <= (0: int) then ([], xq)
   else
     (case pull xq of
       NONE => ([], xq)
@@ -174,7 +174,7 @@
 (*print a sequence, up to "count" elements*)
 fun print print_elem count =
   let
-    fun prnt k xq =
+    fun prnt (k: int) xq =
       if k > count then ()
       else
         (case pull xq of
@@ -229,7 +229,7 @@
 
 fun REPEAT1 f = THEN (f, REPEAT f);
 
-fun INTERVAL f i j x =
+fun INTERVAL f (i: int) j x =
   if i > j then single x
   else op THEN (f j, INTERVAL f i (j - 1)) x;