# HG changeset patch
# User wenzelm
# Date 881305263 -3600
# Node ID 2f0c174036dc1fb1ee8a52bdf8d394700612600c
# Parent  4d84cdb0df423178c8c3ec9d57ba9dac7c87d06d
tmp_name;

diff -r 4d84cdb0df42 -r 2f0c174036dc src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Thu Dec 04 14:11:37 1997 +0100
+++ b/src/Pure/Thy/thy_read.ML	Fri Dec 05 08:01:03 1997 +0100
@@ -49,7 +49,7 @@
        
 
 (*Make name of the TextIO.output ML file for a theory *)
-fun out_name tname = "." ^ tname ^ ".thy.ML";
+fun out_name tname = File.tmp_name (tname ^ ".thy.ML");
 
 
 (*Read a file specified by thy_file containing theory tname*)
diff -r 4d84cdb0df42 -r 2f0c174036dc src/Pure/Thy/use.ML
--- a/src/Pure/Thy/use.ML	Thu Dec 04 14:11:37 1997 +0100
+++ b/src/Pure/Thy/use.ML	Fri Dec 05 08:01:03 1997 +0100
@@ -44,7 +44,7 @@
         if txt = txt_out then use_orig name
         else
           let
-            val tmp_name = File.tmp_name (Path.base_name name);
+            val tmp_name = File.tmp_name ("." ^ Path.base_name name);
             val _ = File.write tmp_name txt_out;
             val rm = OS.FileSys.remove;
           in