diff -r a63d76ba0a03 -r c17253cad5c6 src/HOL/Mirabelle/Tools/mirabelle.ML
--- a/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed May 12 12:22:44 2021 +0200
+++ b/src/HOL/Mirabelle/Tools/mirabelle.ML	Wed May 12 13:10:13 2021 +0200
@@ -68,15 +68,15 @@
 )
 
 
-fun log_exn log tag id e = log (tag id ^ "exception:\n" ^ General.exnMessage e)
+fun exn_log tag id e = tag id ^ "exception:\n" ^ General.exnMessage e
 
-fun catch tag f id (st as {log, ...}: run_args) = (f id st; ())
+fun catch tag f id (args: run_args) = f id args
   handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; ())
+    if Exn.is_interrupt exn then Exn.reraise exn else #log args (exn_log tag id exn)
 
-fun catch_result tag d f id (st as {log, ...}: run_args) = f id st
+fun catch_result tag default f id (args: run_args) = f id args
   handle exn =>
-    if Exn.is_interrupt exn then Exn.reraise exn else (log_exn log tag id exn; d)
+    if Exn.is_interrupt exn then Exn.reraise exn else (#log args (exn_log tag id exn); default)
 
 fun register (init, run, done) thy =
   let val id = length (Actions.get thy) + 1