--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Fri Oct 15 12:42:51 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Oct 18 11:11:22 2021 +0200
@@ -231,7 +231,10 @@
(* initialize actions *)
val contexts = actions |> map_index (fn (n, (label, name, args)) =>
let
- val make_action = the (get_action name);
+ val make_action =
+ (case get_action name of
+ SOME f => f
+ | NONE => error "Unknown action");
val action_subdir = if label = "" then string_of_int n ^ "." ^ name else label;
val output_dir = Path.append mirabelle_output_dir (Path.basic action_subdir);
val context =