src/Pure/ML-Systems/smlnj.ML
changeset 6227 3198f547f8af
parent 5816 6f3cb53502fa
child 7855 092a6435afad
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Feb 04 18:15:01 1999 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Feb 04 18:15:20 1999 +0100
@@ -192,9 +192,8 @@
 
 (* file handling *)
 
-(*get time of last modification; if file doesn't exist return an empty string*)
-fun file_info "" = ""           (* FIXME !? *)
-  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
+(*get time of last modification*)
+fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
 
 
 (* getenv *)