# 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;