src/Pure/library.ML
changeset 41492 7a4138cb46db
parent 41489 8e2b8649507d
child 41494 364f672d8827
     1.1 --- a/src/Pure/library.ML	Mon Jan 10 15:45:46 2011 +0100
     1.2 +++ b/src/Pure/library.ML	Mon Jan 10 16:07:16 2011 +0100
     1.3 @@ -642,7 +642,19 @@
     1.4    in implode (map chrof (radixpand (base, num))) end;
     1.5  
     1.6  
     1.7 -val string_of_int = Int.toString;
     1.8 +local
     1.9 +  val zero = ord "0";
    1.10 +  val small = 10000;
    1.11 +  val small_table = Vector.tabulate (small, Int.toString);
    1.12 +in
    1.13 +
    1.14 +fun string_of_int i =
    1.15 +  if i < 0 then Int.toString i
    1.16 +  else if i < 10 then chr (zero + i)
    1.17 +  else if i < small then Vector.sub (small_table, i)
    1.18 +  else Int.toString i;
    1.19 +
    1.20 +end;
    1.21  
    1.22  fun signed_string_of_int i =
    1.23    if i < 0 then "-" ^ string_of_int (~ i) else string_of_int i;