# HG changeset patch
# User paulson
# Date 849608507 -3600
# Node ID 618b545fe9c433609a5b70d8cf3288ecfaeb8616
# Parent  84ed9e0d7c504227c296ce49ea767e6f2d4b0ff1
Simplified file_info using OS.FileSys instead of Posix.FileSys
(also for MLWorks compatibility)

diff -r 84ed9e0d7c50 -r 618b545fe9c4 src/Pure/NJ1xx.ML
--- a/src/Pure/NJ1xx.ML	Tue Dec 03 11:20:43 1996 +0100
+++ b/src/Pure/NJ1xx.ML	Tue Dec 03 11:21:47 1996 +0100
@@ -79,9 +79,7 @@
 
 (*Get time of last modification; if file doesn't exist return an empty string*)
 fun file_info "" = ""
-  | file_info name = Time.toString
-			 (Posix.FileSys.ST.mtime (Posix.FileSys.stat name))  
-		     handle _ => "";
+  | file_info name = Time.toString (OS.FileSys.modTime name) handle _ =>"";