--- 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 ^ " ****"))
);