--- 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 "" ::