--- a/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Wed Dec 15 23:18:41 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_arith.ML Fri Dec 17 09:51:37 2021 +0100
@@ -16,7 +16,7 @@
(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
+ in ("", {run_action = run_action, finalize = K ""}) end
val () = Mirabelle.register_action "arith" make_action