# HG changeset patch
# User blanchet
# Date 1283379353 -7200
# Node ID 344028ecc00ee00c45336aa543057ad84593dc3a
# Parent  a9a2efcaf7217bf11b37ca59382c31a9142447c0
show real CPU time

diff -r a9a2efcaf721 -r 344028ecc00e src/HOL/Tools/ATP/atp_systems.ML
--- a/src/HOL/Tools/ATP/atp_systems.ML	Wed Sep 01 23:55:59 2010 +0200
+++ b/src/HOL/Tools/ATP/atp_systems.ML	Thu Sep 02 00:15:53 2010 +0200
@@ -247,8 +247,8 @@
 
 fun the_system name versions =
   case get_system name versions of
-    NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
-  | SOME sys => sys
+    SOME sys => sys
+  | NONE => error ("System " ^ quote name ^ " not available at SystemOnTPTP.")
 
 fun remote_config system_name system_versions proof_delims known_failures
                   default_max_relevant use_conjecture_for_hypotheses
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, [])