--- 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
--- 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, [])