# HG changeset patch
# User wenzelm
# Date 1120672840 -7200
# Node ID c4c9d5df26ba70a7bac3b03b229263701fb2ccdf
# Parent  e264077b68a70304ea160469469c3ad7300b02f2
finish: Output.accumulated_time;

diff -r e264077b68a7 -r c4c9d5df26ba src/Pure/Isar/session.ML
--- a/src/Pure/Isar/session.ML	Wed Jul 06 20:00:39 2005 +0200
+++ b/src/Pure/Isar/session.ML	Wed Jul 06 20:00:40 2005 +0200
@@ -58,7 +58,8 @@
 (* finish *)
 
 fun finish () =
-  (ThyInfo.finish ();
+  (Output.accumulated_time ();
+    ThyInfo.finish ();
     Present.finish ();
     session_finished := true);