--- a/src/Pure/Concurrent/future.ML Fri Feb 18 16:07:32 2011 +0100
+++ b/src/Pure/Concurrent/future.ML Fri Feb 18 16:11:58 2011 +0100
@@ -203,7 +203,7 @@
Task_Queue.running task (fn () =>
setmp_worker_task task (fn () =>
fold (fn job => fn ok => job valid andalso ok) jobs true) ());
- val _ = Multithreading.tracing 1 (fn () =>
+ val _ = Multithreading.tracing 2 (fn () =>
let
val s = Task_Queue.str_of_task task;
fun micros time = string_of_int (Time.toNanoseconds time div 1000);
--- a/src/Pure/goal.ML Fri Feb 18 16:07:32 2011 +0100
+++ b/src/Pure/goal.ML Fri Feb 18 16:11:58 2011 +0100
@@ -115,7 +115,7 @@
let
val n = m + i;
val _ =
- Multithreading.tracing 1 (fn () =>
+ Multithreading.tracing 2 (fn () =>
("PROOFS " ^ Time.toString (Time.now ()) ^ ": " ^ string_of_int n));
in n end);