src/Pure/POLY.ML

   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) *)
+(*Get time of last modification; if file doesn't exist return an empty string*)
 fun file_info "" = ""
-  | file_info name = radixstring (System.filedate name);
+  | file_info name = radixstring (System.filedate name)  handle _ => "";
 
 (*Delete a file *)
 fun delete_file name =
   let val (is, os) = ExtendedIO.execute ("rm " ^ name)
   in close_in is;