# HG changeset patch
# User wenzelm
# Date 1245251246 -7200
# Node ID 0d2f700fe5e7c0652ca125563a1ebe17f45a373e
# Parent  e54ae15335a13cd1ac82c40865ee2fffc84bee16
more detailed start_timing/end_timing;

diff -r e54ae15335a1 -r 0d2f700fe5e7 src/Pure/Tools/find_consts.ML
--- a/src/Pure/Tools/find_consts.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/Tools/find_consts.ML	Wed Jun 17 17:07:26 2009 +0200
@@ -128,7 +128,7 @@
       |> sort (rev_order o int_ord o pairself snd)
       |> map (apsnd fst o fst);
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
       :: Pretty.str ""
diff -r e54ae15335a1 -r 0d2f700fe5e7 src/Pure/Tools/find_theorems.ML
--- a/src/Pure/Tools/find_theorems.ML	Wed Jun 17 17:06:07 2009 +0200
+++ b/src/Pure/Tools/find_theorems.ML	Wed Jun 17 17:07:26 2009 +0200
@@ -427,7 +427,7 @@
              then " (" ^ string_of_int returned ^ " displayed)"
              else ""));
 
-    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
+    val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
         :: Pretty.str "" ::