--- a/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_try0.ML Sat Jan 22 11:46:25 2022 +0100
@@ -13,12 +13,12 @@
let
val generous_timeout = Time.scale 10.0 timeout
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
if Timeout.apply generous_timeout (Try0.try0 (SOME timeout) ([], [], [], [])) pre then
"succeeded"
else
""
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "try0" make_action