# HG changeset patch
# User wenzelm
# Date 1330360774 -3600
# Node ID e6e1ec6d5c1c3c66a65f9b5aa894450212fd8a92
# Parent  8650d9a957364d0310c970e60b598e5fef72509e
prefer uniform Timing.message -- avoid assumption about sequential execution;

diff -r 8650d9a95736 -r e6e1ec6d5c1c src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- 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
diff -r 8650d9a95736 -r e6e1ec6d5c1c src/Pure/Tools/find_consts.ML
--- 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 "" ::
diff -r 8650d9a95736 -r e6e1ec6d5c1c src/Pure/Tools/find_theorems.ML
--- 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 "" ::