option parallel_proofs_reuse_timing controls reuse of log information -- since it is not always beneficial for performance;

--- a/etc/options	Wed Feb 20 18:04:44 2013 +0100
+++ b/etc/options	Wed Feb 20 19:57:17 2013 +0100
@@ -53,6 +53,8 @@
   -- "level of parallel proof checking: 0, 1, 2"
 option parallel_proofs_threshold : int = 100
   -- "threshold for sub-proof parallelization"
+option parallel_proofs_reuse_timing : bool = true
+  -- "reuse timing information from old log file for parallel proof scheduling"
 
 
 section "Detail of Proof Recording"

--- a/src/Pure/Tools/build.scala	Wed Feb 20 18:04:44 2013 +0100
+++ b/src/Pure/Tools/build.scala	Wed Feb 20 19:57:17 2013 +0100
@@ -288,12 +288,14 @@
 
   object Queue
   {
-    def apply(tree: Session_Tree, get_timings: String => (List[Properties.T], Double)): Queue =
+    def apply(tree: Session_Tree, load_timings: String => (List[Properties.T], Double)): Queue =
     {
       val graph = tree.graph
       val sessions = graph.keys.toList
 
-      val timings = sessions.map(name => (name, get_timings(name)))
+      val timings = sessions.map((name: String) =>
+        if (tree(name).options.bool("parallel_proofs_reuse_timing")) (name, load_timings(name))
+        else (name, (Nil, 0.0)))
       val command_timings =
         Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
       val session_timing =
@@ -680,7 +682,7 @@
 
     /* queue with scheduling information */
 
-    def get_timing(name: String): (List[Properties.T], Double) =
+    def load_timings(name: String): (List[Properties.T], Double) =
     {
       val (path, text) =
         find_log(name + ".gz") match {
@@ -703,7 +705,7 @@
       }
     }
 
-    val queue = Queue(selected_tree, get_timing)
+    val queue = Queue(selected_tree, load_timings)
 
 
     /* main build process */