diff -r 0e8b45a7d104 -r 9ea709aa275c src/Pure/Thy/thy_read.ML
--- a/src/Pure/Thy/thy_read.ML	Mon Oct 05 10:31:43 1998 +0200
+++ b/src/Pure/Thy/thy_read.ML	Mon Oct 05 10:33:34 1998 +0200
@@ -249,12 +249,7 @@
 	     (writeln ("Reading \"" ^ name ^ ".thy\"");
 	      init_thyinfo ();
 	      read_thy tname thy_file;
-              let val old_pt = ! Goals.proof_timing;
-	      in  (*suppress annoying messages during theory loading*)
-		  proof_timing := false;
-		  Use.use (out_name tname);
-                  proof_timing := old_pt
-                  end;
+	      Use.use (out_name tname);
 	      if not (!delete_tmpfiles) then ()
 	      else OS.FileSys.remove (out_name tname);
 	      thyfile2html tname abs_path)
@@ -294,7 +289,7 @@
 
 fun time_use_thy tname = timeit(fn()=>
    (writeln("\n**** Starting Theory " ^ tname ^ " ****");
-    use_thy tname;
+    setmp Goals.proof_timing true use_thy tname;
     writeln("\n**** Finished Theory " ^ tname ^ " ****"))
    );