--- a/src/Pure/POLY.ML Mon Jan 15 14:47:56 1996 +0100
+++ b/src/Pure/POLY.ML Mon Jan 15 14:56:38 1996 +0100
@@ -55,23 +55,21 @@
| 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 a string containing the time of last modification, attributes, owner
and size of file (but not the path) *)
fun file_info "" = ""
- | file_info name =
- let 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 val offset = ord "0";
- fun chrof n = chr (offset + n);
- in implode (map chrof (radixpand num)) end;
- in radixstring (System.filedate name) end;
+ | file_info name = radixstring (System.filedate name);
(*Delete a file *)
fun delete_file name =