# HG changeset patch
# User clasohm
# Date 769349197 -7200
# Node ID c1e3c8508fd2da4a89b07ca4156fe07b6dd02545
# Parent  85ff48546a05a47722903f90c274793c6f442f72
use_thy now uses use_string instead of creating a temporary file

diff -r 85ff48546a05 -r c1e3c8508fd2 src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Thu May 19 13:45:50 1994 +0200
+++ b/src/Pure/Thy/read.ML	Thu May 19 14:06:37 1994 +0200
@@ -259,13 +259,8 @@
          else (writeln ("Reading \"" ^ name ^ ".ML\"");
                use ml_file);
 
-         let val outstream = open_out ".tmp.ML"
-         in
-             output (outstream, "store_theory " ^ quote thy_name ^ " "
-                                ^ thy_name ^ ".thy;\n");
-             close_out outstream 
-         end;
-         use ".tmp.ML";
+         use_string ("store_theory " ^ quote thy_name ^ " " 
+                     ^ thy_name ^ ".thy");
 
          (*Now set the correct info*)
          set_info (file_info thy_file) (file_info ml_file) thy_name;
@@ -277,8 +272,7 @@
          (*Remove temporary files*)
          if not (!delete_tmpfiles) orelse (thy_file = "") orelse thy_uptodate 
            then ()
-         else delete_file (out_name thy_name);
-         delete_file ".tmp.ML"
+         else delete_file (out_name thy_name)
         )
     end;
 
@@ -455,5 +449,4 @@
                       theory = Some thy}]
   in loaded_thys := make_change (!loaded_thys) end;
 
-end
-
+end;