src/Pure/library.ML
changeset 24630 351a308ab58d
parent 24593 1547ea587f5a
child 24846 d8ff870a11ff
     1.1 --- a/src/Pure/library.ML	Tue Sep 18 11:06:22 2007 +0200
     1.2 +++ b/src/Pure/library.ML	Tue Sep 18 16:08:00 2007 +0200
     1.3 @@ -125,7 +125,7 @@
     1.4    val string_of_int: int -> string
     1.5    val signed_string_of_int: int -> string
     1.6    val string_of_indexname: string * int -> string
     1.7 -  val read_intinf: int -> string list -> IntInf.int * string list
     1.8 +  val read_radix_int: int -> string list -> int * string list
     1.9    val read_int: string list -> int * string list
    1.10    val oct_char: string -> string
    1.11  
    1.12 @@ -640,20 +640,20 @@
    1.13  
    1.14  (* read integers *)
    1.15  
    1.16 -fun read_intinf radix cs =
    1.17 +fun read_radix_int radix cs =
    1.18    let
    1.19      val zero = ord "0";
    1.20      val limit = zero + radix;
    1.21      fun scan (num, []) = (num, [])
    1.22        | scan (num, c :: cs) =
    1.23          if zero <= ord c andalso ord c < limit then
    1.24 -          scan (IntInf.fromInt radix * num + IntInf.fromInt (ord c - zero), cs)
    1.25 +          scan (radix * num + (ord c - zero), cs)
    1.26          else (num, c :: cs);
    1.27 -  in scan (IntInf.fromInt 0, cs) end;
    1.28 +  in scan (0, cs) end;
    1.29  
    1.30 -fun read_int cs = apfst IntInf.toInt (read_intinf 10 cs);
    1.31 +val read_int = read_radix_int 10;
    1.32  
    1.33 -fun oct_char s = chr (IntInf.toInt (#1 (read_intinf 8 (explode s))));
    1.34 +fun oct_char s = chr (#1 (read_radix_int 8 (explode s)));
    1.35  
    1.36  
    1.37