--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Jan 11 17:02:52 2023 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Thu Jan 12 15:46:44 2023 +0100
@@ -305,12 +305,14 @@
exhaustive_preplay proof_method_from_msg thy_index trivial pos st =
let
val thy = Proof.theory_of st
- val thy_name = Context.theory_name thy
+ val thy_long_name = Context.theory_long_name thy
+ val session_name = Long_Name.qualifier thy_long_name
+ val thy_name = Long_Name.base_name thy_long_name
val triv_str = if trivial then "[T] " else ""
val keep =
if keep_probs orelse keep_proofs then
let val subdir = StringCvt.padLeft #"0" 4 (string_of_int thy_index) ^ "_" ^ thy_name in
- Path.append output_dir (Path.basic subdir)
+ Path.append (Path.append output_dir (Path.basic session_name)) (Path.basic subdir)
|> Isabelle_System.make_directory
|> Path.implode
|> (fn dir => SOME (dir, keep_probs, keep_proofs))