--- a/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Sat Jan 22 11:33:31 2022 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_quickcheck.ML Sat Jan 22 11:46:25 2022 +0100
@@ -15,11 +15,11 @@
val quickcheck =
Quickcheck.quickcheck (map (apsnd single) (filter has_valid_key arguments)) 1
- fun run_action ({pre, ...} : Mirabelle.command) =
+ fun run ({pre, ...} : Mirabelle.command) =
(case Timeout.apply timeout quickcheck pre of
NONE => "no counterexample"
| SOME _ => "counterexample found")
- in ("", {run_action = run_action, finalize = K ""}) end
+ in ("", {run = run, finalize = K ""}) end
val () = Mirabelle.register_action "quickcheck" make_action