moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
authorclasohm
Wed, 16 Feb 1994 09:22:15 +0100
changeset 269 237d57b956c1
parent 268 1a038ec6f923
child 270 d506ea00c825
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Mon Feb 14 17:59:25 1994 +0100
+++ b/src/Pure/Thy/read.ML	Wed Feb 16 09:22:15 1994 +0100
@@ -269,19 +269,19 @@
              close_out outstream 
          end;
          use ".tmp.ML";
-         delete_file ".tmp.ML";
 
-         (*Now set the correct info.*)
+         (*Now set the correct info*)
          set_info (file_info thy_file) (file_info ml_file) thy_name;
          set_path ();
 
-         (*Mark theories that have to be reloaded.*)
+         (*Mark theories that have to be reloaded*)
          mark_children thy_name;
 
-         if not (!delete_tmpfiles) orelse (thy_file = "") 
-            orelse thy_uptodate 
-         then ()
-         else delete_file (out_name thyl)
+         (*Remove temporary files*)
+         if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
+           then ()
+         else delete_file (out_name thyl);
+         delete_file ".tmp.ML"
         )
     end;