equal
deleted
inserted
replaced
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 |