# HG changeset patch
# User paulson
# Date 865510112 -7200
# Node ID 131262e21ada3f35c71c90f093126ec58ca01c35
# Parent  2cccd0e3e9ea7847e160e89803e67d8dd6e903e6
There was never need for another copy of radixstring...

diff -r 2cccd0e3e9ea -r 131262e21ada 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 =