src/Pure/library.ML
changeset 41494 364f672d8827
parent 41492 7a4138cb46db
child 41516 3a70387b5e01
equal deleted inserted replaced
41493:f05976d69141 41494:364f672d8827
   642   in implode (map chrof (radixpand (base, num))) end;
   642   in implode (map chrof (radixpand (base, num))) end;
   643 
   643 
   644 
   644 
   645 local
   645 local
   646   val zero = ord "0";
   646   val zero = ord "0";
   647   val small = 10000;
   647   val small = 10000: int;
   648   val small_table = Vector.tabulate (small, Int.toString);
   648   val small_table = Vector.tabulate (small, Int.toString);
   649 in
   649 in
   650 
   650 
   651 fun string_of_int i =
   651 fun string_of_int i =
   652   if i < 0 then Int.toString i
   652   if i < 0 then Int.toString i