prefer uniform Timing.message -- avoid assumption about sequential execution;

--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 17:13:25 2012 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Mon Feb 27 17:39:34 2012 +0100
@@ -97,7 +97,7 @@
     val end_msg = "Checked " ^ string_of_int with_assumptions ^ " theorem(s) with assumptions"
       ^ " in the theory " ^ quote thy_name
       ^ " with a total of " ^ string_of_int total ^ " theorem(s)"  
-      ^ " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
+      ^ " in " ^ Timing.message (Timing.result start);
   in
     ([Pretty.str (msg ^ ":"), Pretty.str ""] @
         map pretty_thm with_superfluous_assumptions

--- a/src/Pure/Tools/find_consts.ML	Mon Feb 27 17:13:25 2012 +0100
+++ b/src/Pure/Tools/find_consts.ML	Mon Feb 27 17:39:34 2012 +0100
@@ -114,7 +114,7 @@
       |> sort (rev_order o int_ord o pairself snd)
       |> map (apsnd fst o fst);
 
-    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
+    val end_msg = " in " ^ Timing.message (Timing.result start);
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
     Pretty.str "" ::

--- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:13:25 2012 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:39:34 2012 +0100
@@ -602,7 +602,7 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
-    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
+    val end_msg = " in " ^ Timing.message (Timing.result start);
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
     Pretty.str "" ::