changeset 31687 | 0d2f700fe5e7 |
parent 31684 | d5d830979a54 |
child 32091 | 30e2ffbba718 |
--- a/src/Pure/Tools/find_theorems.ML Wed Jun 17 17:06:07 2009 +0200 +++ b/src/Pure/Tools/find_theorems.ML Wed Jun 17 17:07:26 2009 +0200 @@ -427,7 +427,7 @@ then " (" ^ string_of_int returned ^ " displayed)" else "")); - val end_msg = " in " ^ Time.toString (#all (end_timing start)) ^ " secs"; + val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs"; in Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) :: Pretty.str "" ::