src/Pure/Tools/find_consts.ML
changeset 30188 82144a95f9ec
parent 30143 98a986b02022
child 30190 479806475f3c
     1.1 --- a/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:21:33 2009 +0100
     1.2 +++ b/src/Pure/Tools/find_consts.ML	Sun Mar 01 16:22:37 2009 +0100
     1.3 @@ -119,9 +119,7 @@
     1.4        |> sort (rev_order o int_ord o pairself snd)
     1.5        |> map ((apsnd fst) o fst);
     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 raw_criteria)
    1.13        :: Pretty.str ""