--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Sat Jun 12 12:16:19 2021 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Sat Jun 12 12:39:33 2021 +0200
@@ -53,7 +53,10 @@
(Symtab.empty : (action_context -> action) Symtab.table);
in
-val register_action = Synchronized.change actions oo curry Symtab.update;
+fun register_action name make_action =
+ (if name = "" then error "Registering unnamed Mirabelle action" else ();
+ Synchronized.change actions (Symtab.map_default (name, make_action)
+ (fn f => (warning ("Redefining Mirabelle action: " ^ quote name); f))));
fun get_action name = Symtab.lookup (Synchronized.value actions) name;