# HG changeset patch
# User wenzelm
# Date 1298041918 -3600
# Node ID 3bd83302a3c3ad99b96d59a3933430e82457138a
# Parent  6214816d79d30d5ad3ee3c4c5c634b6240f70717
less verbose tracing;

diff -r 6214816d79d3 -r 3bd83302a3c3 src/Pure/Concurrent/future.ML
--- 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);
diff -r 6214816d79d3 -r 3bd83302a3c3 src/Pure/goal.ML
--- 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);