--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Mon Oct 18 11:11:22 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Mon Oct 18 11:11:59 2021 +0200
@@ -13,10 +13,9 @@
fun make_action ({timeout, ...} : Mirabelle.action_context) =
let
fun run_action ({pre, ...} : Mirabelle.command) =
- if Mirabelle.can_apply timeout Arith_Data.arith_tac pre then
- "succeeded"
- else
- ""
+ (case Timing.timing (Mirabelle.can_apply timeout Arith_Data.arith_tac) pre of
+ ({cpu, ...}, true) => "succeeded (" ^ Time.toString cpu ^ " s)"
+ | (_, false) => "failed")
in {run_action = run_action, finalize = K ""} end
val () = Mirabelle.register_action "arith" make_action