src/Pure/Tools/find_theorems.ML
changeset 46713 e6e1ec6d5c1c
parent 43767 e0219ef7f84c
child 46716 c45a4427db39
     1.1 --- a/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:13:25 2012 +0100
     1.2 +++ b/src/Pure/Tools/find_theorems.ML	Mon Feb 27 17:39:34 2012 +0100
     1.3 @@ -602,7 +602,7 @@
     1.4               then " (" ^ string_of_int returned ^ " displayed)"
     1.5               else ""));
     1.6  
     1.7 -    val end_msg = " in " ^ Time.toString (#cpu (Timing.result start)) ^ " secs";
     1.8 +    val end_msg = " in " ^ Timing.message (Timing.result start);
     1.9    in
    1.10      Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
    1.11      Pretty.str "" ::