# HG changeset patch
# User clasohm
# Date 761386935 -3600
# Node ID 237d57b956c19d4fc142c59f2c3a6a243db143b0
# Parent  1a038ec6f92321cc79c65df88001042e5720a582
moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML

diff -r 1a038ec6f923 -r 237d57b956c1 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;