diff -r a9a2efcaf721 -r 344028ecc00e src/HOL/Tools/Sledgehammer/sledgehammer.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Wed Sep 01 23:55:59 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer.ML	Thu Sep 02 00:15:53 2010 +0200
@@ -247,7 +247,7 @@
         val core = File.shell_path command ^ " " ^ arguments complete timeout ^
                    " " ^ File.shell_path probfile
       in
-        (if measure_run_time then "TIMEFORMAT='%3U'; { time " ^ core ^ " ; }"
+        (if measure_run_time then "TIMEFORMAT='%3R'; { time " ^ core ^ " ; }"
          else "exec " ^ core) ^ " 2>&1"
       end
     fun split_time s =
@@ -333,7 +333,7 @@
             (full_types, minimize_command, proof, axiom_names, goal, subgoal)
         |>> (fn message =>
                 message ^ (if verbose then
-                             "\nCPU time: " ^ string_of_int msecs ^ " ms."
+                             "\nReal CPU time: " ^ string_of_int msecs ^ " ms."
                            else
                              ""))
       | SOME failure => (string_for_failure failure, [])