--- a/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Sep 25 19:49:25 2023 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML Mon Sep 25 20:56:44 2023 +0200
@@ -95,9 +95,7 @@
| exn => "exception: " ^ General.exnMessage exn);
fun run_action_function f =
- f () handle exn =>
- if Exn.is_interrupt exn then Exn.reraise exn
- else print_exn exn;
+ \<^try>\<open>f () catch exn => print_exn exn\<close>;
fun make_action_path ({index, label, name, ...} : action_context) =
Path.basic (if label = "" then string_of_int index ^ "." ^ name else label);