delete_file now has type string -> unit in both NJ and POLY,
use of Pure/Thy/ROOT has been moved to the end of Pure/ROOT again

--- a/src/Pure/NJ.ML	Fri Oct 22 13:35:15 1993 +0100
+++ b/src/Pure/NJ.ML	Fri Oct 22 13:39:23 1993 +0100
@@ -90,5 +90,7 @@
     | file_info name = makestring (mtime (PATH name));
 end;
 
-fun delete_file name = System.system ("rm " ^ name);
+fun delete_file name = 
+  let val _ = System.system ("rm " ^ name)
+  in () end;
 

--- a/src/Pure/POLY.ML	Fri Oct 22 13:35:15 1993 +0100
+++ b/src/Pure/POLY.ML	Fri Oct 22 13:39:23 1993 +0100
@@ -60,4 +60,7 @@
            implode result
         end;
 
-fun delete_file name = ExtendedIO.execute ("rm " ^ name);
+(*Delete a file *)
+fun delete_file name =
+  let val (_,_) = ExtendedIO.execute ("rm " ^ name)
+  in () end;

--- a/src/Pure/ROOT.ML	Fri Oct 22 13:35:15 1993 +0100
+++ b/src/Pure/ROOT.ML	Fri Oct 22 13:39:23 1993 +0100
@@ -27,11 +27,6 @@
 use "ROOT.ML";
 cd "..";
 
-(*Theory parser*)
-cd "Thy";
-use "ROOT.ML";
-cd "..";
-
 use "type.ML";
 use "sign.ML";
 use "sequence.ML";
@@ -70,3 +65,12 @@
 
 use "install_pp.ML";
 
+
+
+(*Theory parser
+  (The new Thy/read.ML needs Thm so this has to be done AFTER Thm is
+   created.) *)
+cd "Thy";
+use "ROOT.ML";
+cd "..";
+