--- a/src/Pure/NJ093.ML Fri May 23 14:49:39 1997 +0200
+++ b/src/Pure/NJ093.ML Fri May 23 14:52:45 1997 +0200
@@ -85,7 +85,7 @@
struct
structure FileSys =
struct
- val OS.FileSys.chDir = System.Directory.cd
+ val chDir = System.Directory.cd
val remove = System.Unsafe.SysIO.unlink (*Delete a file *)
val getDir = System.Directory.getWD (*path of working directory*)
end
@@ -110,7 +110,7 @@
open_in tmp_name);
val result = input (is, 999999);
in close_in is;
- delete_file tmp_name;
+ OS.FileSys.remove tmp_name;
result
end;