--- 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*)
--- 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