# HG changeset patch
# User wenzelm
# Date 1166137694 -3600
# Node ID 03e1e75ad2e51f8354874a40c6bc98d9b78b36c3
# Parent  05f57309170c43b63e229717582686ea82672fe5
tuned -- accomodate Alice;

diff -r 05f57309170c -r 03e1e75ad2e5 src/Pure/library.ML
--- a/src/Pure/library.ML	Fri Dec 15 00:08:06 2006 +0100
+++ b/src/Pure/library.ML	Fri Dec 15 00:08:14 2006 +0100
@@ -660,7 +660,7 @@
 
 fun gcd (x, y) =
   let fun gxd x y : IntInf.int =
-    if y = 0 then x else gxd y (x mod y)
+    if y = IntInf.fromInt 0 then x else gxd y (x mod y)
   in if x < y then gxd y x else gxd x y end;
 
 fun lcm (x, y) = (x * y) div gcd (x, y);
@@ -672,12 +672,12 @@
 (* lists of integers *)
 
 (*make the list [from, from + 1, ..., to]*)
-fun (from upto to) =
-  if from > to then [] else from :: ((from + 1) upto to);
+fun (i upto j) =
+  if i > j then [] else i :: (i + 1 upto j);
 
 (*make the list [from, from - 1, ..., to]*)
-fun (from downto to) =
-  if from < to then [] else from :: ((from - 1) downto to);
+fun (i downto j) =
+  if i < j then [] else i :: (i - 1 downto j);
 
 (*predicate: downto0 (is, n) <=> is = [n, n - 1, ..., 0]*)
 fun downto0 (i :: is, n) = i = n andalso downto0 (is, n - 1)
@@ -720,7 +720,7 @@
         if zero <= ord c andalso ord c < limit then
           scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs)
         else (num, c :: cs);
-  in scan (0, cs) end;
+  in scan (IntInf.fromInt 0, cs) end;
 
 fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);