# HG changeset patch
# User wenzelm
# Date 1235920957 -3600
# Node ID 82144a95f9ec8bcdeda4dc7929d19a89318b382d
# Parent  b92b3375e91934a92bae881d4b574e36d0aeec2a
avoid fragile parsing of end_timing result -- would have produced GC time on MosML, for example;

diff -r b92b3375e919 -r 82144a95f9ec src/Pure/Tools/find_consts.ML
--- 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 ""
diff -r b92b3375e919 -r 82144a95f9ec src/Pure/Tools/find_theorems.ML
--- 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 "" ::