# HG changeset patch
# User wenzelm
# Date 1117963890 -7200
# Node ID 7a6616be8712bae60e16988ccfd719aa478c116a
# Parent  ee2497cde564a4e2a4ee7166060750afcd4dfc9c
removed file_info (now in Pure/General/file.ML);

diff -r ee2497cde564 -r 7a6616be8712 src/Pure/ML-Systems/mosml.ML
--- a/src/Pure/ML-Systems/mosml.ML	Sun Jun 05 11:31:29 2005 +0200
+++ b/src/Pure/ML-Systems/mosml.ML	Sun Jun 05 11:31:30 2005 +0200
@@ -124,12 +124,6 @@
   if Process.system cmd = Process.success then 0 else 1;
 
 
-(* file handling *)
-
-(*get time of last modification*)
-fun file_info name = Time.toString (FileSys.modTime name) handle _ => "";
-
-
 (* getenv *)
 
 fun getenv var =
diff -r ee2497cde564 -r 7a6616be8712 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Sun Jun 05 11:31:29 2005 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Sun Jun 05 11:31:30 2005 +0200
@@ -151,12 +151,6 @@
   if OS.Process.isSuccess (OS.Process.system cmd) then 0 else 1;
 
 
-(* file handling *)
-
-(*get time of last modification*)
-fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
-
-
 (* getenv *)
 
 fun getenv var =
diff -r ee2497cde564 -r 7a6616be8712 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Sun Jun 05 11:31:29 2005 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Sun Jun 05 11:31:30 2005 +0200
@@ -180,12 +180,6 @@
 val system = OS.Process.system: string -> int;
 
 
-(* file handling *)
-
-(*get time of last modification*)
-fun file_info name = Time.toString (OS.FileSys.modTime name) handle _ => "";
-
-
 (* getenv *)
 
 fun getenv var =