# HG changeset patch
# User clasohm
# Date 821714198 -3600
# Node ID 2ebbc23d49fa5d36a95c282995a740aea2e65d08
# Parent  88b73ad6b0daf6a80ced4a73665f0060c498da2f
beautified file_info a bit

diff -r 88b73ad6b0da -r 2ebbc23d49fa src/Pure/POLY.ML
--- 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 =