# HG changeset patch
# User desharna
# Date 1752406884 -7200
# Node ID ca4aed6a9eb0a0ea85a91c34e330fe9f765f5941
# Parent  1e39653de9742184321004a757cd26e0a0883d61
tuned

diff -r 1e39653de974 -r ca4aed6a9eb0 src/HOL/Tools/Mirabelle/mirabelle.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle.ML	Sat Jul 12 22:37:47 2025 +0200
+++ b/src/HOL/Tools/Mirabelle/mirabelle.ML	Sun Jul 13 13:41:24 2025 +0200
@@ -130,17 +130,16 @@
 
 fun apply_action ({run, ...} : action) context (command as {pos, pre, ...} : command) =
   let
-    val thy = Proof.theory_of pre;
-    val action_path = make_action_path context;
-    val goal_name_path = Path.basic (#name command)
-    val line_path = Path.basic (string_of_int (the (Position.line_of pos)));
-    val offset_path = Path.basic (string_of_int (the (Position.offset_of pos)));
-    val ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run command);
+    val action_path = make_action_path context
+    and goal_name_path = Path.basic (#name command)
+    and line_path = Path.basic (string_of_int (the (Position.line_of pos)))
+    and offset_path = Path.basic (string_of_int (the (Position.offset_of pos)))
+    and ({elapsed, ...}, s) = Timing.timing run_action_function (fn () => run command);
     val export_name =
       Path.binding0 (Path.basic "mirabelle" + action_path + Path.basic "goal" + goal_name_path +
         line_path + offset_path + Path.basic (string_of_int (Time.toMilliseconds elapsed)));
   in
-    Export.export thy export_name [XML.Text s]
+    Export.export (Proof.theory_of pre) export_name [XML.Text s]
   end;