# HG changeset patch
# User wenzelm
# Date 1152620467 -7200
# Node ID 432e914a0e953e5086ddc3c1b4a7e865b2825efe
# Parent  99f27df2b6d0bbb30783207b425efa77fb13311f
replaced  read_radixint by read_intinf;

diff -r 99f27df2b6d0 -r 432e914a0e95 src/Pure/library.ML
--- a/src/Pure/library.ML	Tue Jul 11 14:21:05 2006 +0200
+++ b/src/Pure/library.ML	Tue Jul 11 14:21:07 2006 +0200
@@ -163,7 +163,7 @@
   val radixstring: int * string * int -> string
   val string_of_int: int -> string
   val string_of_indexname: string * int -> string
-  val read_radixint: int * string list -> int * string list
+  val read_intinf: int -> string list -> IntInf.int * string list
   val read_int: string list -> int * string list
   val oct_char: string -> string
 
@@ -823,19 +823,20 @@
 
 (* read integers *)
 
-fun read_radixint (radix: int, cs) : int * string list =
-  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(radix*num + ord c - zero, cs)
-              else (num, c::cs)
-  in  scan(0,cs)  end;
+fun read_intinf 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)
+        else (num, c :: cs);
+  in scan (0, cs) end;
 
-fun read_int cs = read_radixint (10, cs);
+fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);
 
-fun oct_char s = chr (#1 (read_radixint (8, explode s)));
+fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));