# HG changeset patch
# User wenzelm
# Date 1343119476 -7200
# Node ID 96c1ef26aabec2b24553f60303778c9b611400d3
# Parent  20170ae271a5d7ffd809b9e8633e657d1c82ef97
timing for whole session;

diff -r 20170ae271a5 -r 96c1ef26aabe src/Pure/System/build.ML
--- a/src/Pure/System/build.ML	Tue Jul 24 10:43:13 2012 +0200
+++ b/src/Pure/System/build.ML	Tue Jul 24 10:44:36 2012 +0200
@@ -49,7 +49,7 @@
         ""
         verbose;
 
-    val _ = List.app (uncurry (use_theories |> Session.with_timing name timing)) theories;
+    val _ = Session.with_timing name timing (List.app (uncurry use_theories)) theories;
     val _ = Session.finish ();
 
     val _ = if save then () else quit ();