tuned;

--- a/src/Pure/Thy/symbol_input.ML	Wed Aug 06 14:10:22 1997 +0200
+++ b/src/Pure/Thy/symbol_input.ML	Wed Aug 06 14:11:08 1997 +0200
@@ -26,21 +26,14 @@
     fn raw_name =>
       let
         val name = fix_name raw_name;
-
-        val infile = TextIO.openIn name;
-        val txt = TextIO.inputAll infile;
-        val _ = TextIO.closeIn infile;
-
+        val txt = read_file name;
         val txt_out = implode (SymbolFont.write_charnames' (explode txt));
       in
         if txt = txt_out then use name
         else
           let
             val tmp_name = "/tmp/" ^ base_name name;  (* FIXME unique prefix (!?) *)
-            val outfile = TextIO.openOut tmp_name;
-            val _ = TextIO.output (outfile, txt_out);
-            val _ = TextIO.closeOut outfile;
-
+            val _ = write_file tmp_name txt_out;
             val rm = OS.FileSys.remove;
           in
             use tmp_name handle exn => (rm tmp_name; raise exn);

--- a/src/Pure/Thy/thy_read.ML	Wed Aug 06 14:10:22 1997 +0200
+++ b/src/Pure/Thy/thy_read.ML	Wed Aug 06 14:11:08 1997 +0200
@@ -28,7 +28,7 @@
 structure ThyRead: THY_READ =
 struct
 
-open ThmDB ThyInfo BrowserInfo;
+open ThmDatabase ThyInfo BrowserInfo;
 
 
 datatype basetype = Thy  of string
@@ -52,17 +52,14 @@
 fun out_name tname = "." ^ tname ^ ".thy.ML";
 
 
-(*Read a file specified by thy_file containing theory thy *)
+(*Read a file specified by thy_file containing theory tname*)
 fun read_thy tname thy_file =
   let
-    val instream  = TextIO.openIn thy_file;
-    val intext = TextIO.inputAll instream;
-    val _ = TextIO.closeIn instream;
+    val intext = read_file thy_file;
     val outext = ThySyn.parse tname intext;
-    val outstream = TextIO.openOut (out_name tname);
-    val _ = TextIO.output (outstream, outext);
-    val _ = TextIO.closeOut outstream;
-  in () end;
+  in
+    write_file (out_name tname) outext
+  end;
 
 
 (*Check if a theory was completly loaded *)