src/HOL/Tools/Mirabelle/mirabelle.ML

       ()
   end
 
 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;
 
 
 (* theory line range *)