# HG changeset patch
# User nipkow
# Date 757794439 -3600
# Node ID b2cdb675ef449e1240e1bb63a35621650cf9b64f
# Parent  7ab45715c0a6d7624fe19f9514aaecd3e6cb9dce
shortened msg

diff -r 7ab45715c0a6 -r b2cdb675ef44 src/Pure/Thy/read.ML
--- a/src/Pure/Thy/read.ML	Tue Jan 04 17:03:52 1994 +0100
+++ b/src/Pure/Thy/read.ML	Wed Jan 05 19:27:19 1994 +0100
@@ -249,13 +249,13 @@
        else
        (
          if thy_uptodate orelse thy_file = "" then ()
-         else (writeln ("Reading thy-file \"" ^ thyl ^ ".thy\"");
+         else (writeln ("Reading \"" ^ thyl ^ ".thy\"");
                read_thy thyl thy_file;
                use (out_name thyl)
               );
 
          if ml_file = "" then () 
-         else (writeln ("Reading ML-file \"" ^ thyl ^ ".ML\"");
+         else (writeln ("Reading \"" ^ thyl ^ ".ML\"");
                use ml_file);
 
          let val outstream = open_out ".tmp.ML"