There was never need for another copy of radixstring...
authorpaulson
Thu Jun 05 13:28:32 1997 +0200 (1997-06-05)
changeset 3406131262e21ada
parent 3405 2cccd0e3e9ea
child 3407 afd288caf573
There was never need for another copy of radixstring...
src/Pure/POLY.ML
     1.1 --- a/src/Pure/POLY.ML	Thu Jun 05 13:27:28 1997 +0200
     1.2 +++ b/src/Pure/POLY.ML	Thu Jun 05 13:28:32 1997 +0200
     1.3 @@ -56,20 +56,11 @@
     1.4          | seqf (x :: xs) = (proc x; seqf xs)
     1.5    in seqf end;
     1.6  
     1.7 -fun radixpand num : int list =
     1.8 -  let fun radix (n, tail) =
     1.9 -    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
    1.10 -  in radix (num, []) end;
    1.11 -
    1.12 -fun radixstring num =
    1.13 -  let fun chrof n = chr (ord "0" + n);
    1.14 -  in implode (map chrof (radixpand num)) end;
    1.15 -
    1.16  in
    1.17  
    1.18  (*Get time of last modification; if file doesn't exist return an empty string*)
    1.19  fun file_info "" = ""
    1.20 -  | file_info name = radixstring (System.filedate name)  handle _ => "";
    1.21 +  | file_info name = makestring (System.filedate name)  handle _ => "";
    1.22  
    1.23  
    1.24  structure OS =