avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

--- a/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:21:33 2009 +0100
+++ b/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:22:37 2009 +0100
@@ -119,9 +119,7 @@
       |> sort (rev_order o int_ord o pairself snd)
       |> map ((apsnd fst) o fst);
 
-    val end_msg = " in " ^
-                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
-                  ^ " secs"
+    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
       :: Pretty.str ""

--- a/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:21:33 2009 +0100
+++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:22:37 2009 +0100
@@ -372,9 +372,7 @@
     val lim = the_default (! limit) opt_limit;
     val thms = Library.drop (len - lim, matches);
 
-    val end_msg = " in " ^
-                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
-                  ^ " secs"
+    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
   in
     Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
         :: Pretty.str "" ::