src/Pure/library.ML

--- a/src/Pure/library.ML	Tue Sep 18 11:06:22 2007 +0200
+++ b/src/Pure/library.ML	Tue Sep 18 16:08:00 2007 +0200
@@ -125,7 +125,7 @@
   val string_of_int: int -> string
   val signed_string_of_int: int -> string
   val string_of_indexname: string * int -> string
-  val read_intinf: int -> string list -> IntInf.int * string list
+  val read_radix_int: int -> string list -> int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string
 
@@ -640,20 +640,20 @@
 
 (* read integers *)
 
-fun read_intinf radix cs =
+fun read_radix_int radix cs =
   let
     val zero = ord "0";
     val limit = zero + radix;
     fun scan (num, []) = (num, [])
       | scan (num, c :: cs) =
         if zero <= ord c andalso ord c < limit then
-          scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs)
+          scan (radix * num + (ord c - zero), cs)
         else (num, c :: cs);
-  in scan (IntInf.fromInt 0, cs) end;
+  in scan (0, cs) end;
 
-fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);
+val read_int = read_radix_int 10;
 
-fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));
+fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));