src/Pure/Tools/find_theorems.ML
changeset 30188 82144a95f9ec
parent 30186 1f836e949ac2
child 30216 0300b7420b07
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:21:33 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Sun Mar 01 16:22:37 2009 +0100
     1.3 @@ -372,9 +372,7 @@
     1.4      val lim = the_default (! limit) opt_limit;
     1.5      val thms = Library.drop (len - lim, matches);
     1.6  
     1.7 -    val end_msg = " in " ^
     1.8 -                  (List.nth (String.tokens Char.isSpace (end_timing start), 3))
     1.9 -                  ^ " secs"
    1.10 +    val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs";
    1.11    in
    1.12      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
    1.13          :: Pretty.str "" ::