# HG changeset patch
# User wenzelm
# Date 864391965 -7200
# Node ID 0206e7507737d25e454a7e3289c6cb2e448483ee
# Parent  0cdbca0a257304056b11f22335f394b1dd4c0170
fixed;

diff -r 0cdbca0a2573 -r 0206e7507737 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;