fixed;
authorwenzelm
Fri, 23 May 1997 14:52:45 +0200
changeset 3319 0206e7507737
parent 3318 0cdbca0a2573
child 3320 3a5e4930fb77
fixed;
src/Pure/NJ093.ML
--- 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;