--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Oct 01 11:17:35 2025 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML Wed Oct 01 11:18:23 2025 +0000
@@ -139,7 +139,11 @@
Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
#> (keep_probs ? Config.put Sledgehammer_Prover_ATP.atp_problem_dest_dir dir)
#> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
- #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+ #> (keep_probs ? Config.put SMT_Config.problem_dest_file
+ (dir ^ "/" ^ filename ^ "__" ^ serial_string ()))
+ #> (keep_proofs ? Config.put Sledgehammer_Prover_ATP.atp_proof_dest_dir dir)
+ #> Config.put SMT_Config.proof_dest_file
+ (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
end
| set_file_name NONE = I
val state' = state