--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Fri Jan 21 21:10:34 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Sat Jan 22 08:46:37 2022 +0100
@@ -329,7 +329,7 @@
val prover_name = hd provers
val (sledgehamer_outcome, msg, cpu_time) =
run_sh params e_selection_heuristic term_order force_sos keep pos st
- val (outcome_msg, change_data, proof_method_and_used_thms) =
+ val (time_prover, change_data, proof_method_and_used_thms) =
(case sledgehamer_outcome of
Sledgehammer.SH_Some {used_facts, run_time, ...} =>
let
@@ -339,9 +339,6 @@
try (Sledgehammer_Util.thms_of_name (Proof.context_of st))
name
|> Option.map (pair (name, stature))
- val outcome_msg =
- " (" ^ string_of_int cpu_time ^ "+" ^ string_of_int time_prover ^ ")" ^
- " [" ^ prover_name ^ "]:\n"
val change_data =
inc_sh_success
#> not trivial ? inc_sh_nontriv_success
@@ -349,10 +346,14 @@
#> inc_sh_max_lems num_used_facts
#> inc_sh_time_prover time_prover
in
- (outcome_msg, change_data,
+ (SOME time_prover, change_data,
SOME (proof_method_from_msg msg, map_filter get_thms used_facts))
end
- | _ => ("", I, NONE))
+ | _ => (NONE, I, NONE))
+ val outcome_msg =
+ "(SH " ^ string_of_int cpu_time ^ "ms" ^
+ (case time_prover of NONE => "" | SOME ms => ", ATP " ^ string_of_int ms ^ "ms") ^
+ ") [" ^ prover_name ^ "]: "
in
(sledgehamer_outcome, triv_str ^ outcome_msg ^ msg, change_data #> inc_sh_time_isa cpu_time,
proof_method_and_used_thms)