There was never need for another copy of radixstring...
authorpaulson
Thu, 05 Jun 1997 13:28:32 +0200
changeset 3406 131262e21ada
parent 3405 2cccd0e3e9ea
child 3407 afd288caf573
There was never need for another copy of radixstring...
src/Pure/POLY.ML
--- a/src/Pure/POLY.ML	Thu Jun 05 13:27:28 1997 +0200
+++ b/src/Pure/POLY.ML	Thu Jun 05 13:28:32 1997 +0200
@@ -56,20 +56,11 @@
         | seqf (x :: xs) = (proc x; seqf xs)
   in seqf end;
 
-fun radixpand num : int list =
-  let fun radix (n, tail) =
-    if n < 10 then n :: tail else radix (n div 10, (n mod 10) :: tail)
-  in radix (num, []) end;
-
-fun radixstring num =
-  let fun chrof n = chr (ord "0" + n);
-  in implode (map chrof (radixpand num)) end;
-
 in
 
 (*Get time of last modification; if file doesn't exist return an empty string*)
 fun file_info "" = ""
-  | file_info name = radixstring (System.filedate name)  handle _ => "";
+  | file_info name = makestring (System.filedate name)  handle _ => "";
 
 
 structure OS =