Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
changeset 83239 0da2f7981483
parent 83238 e6cd54ebb64b 
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Oct 01 11:18:23 2025 +0000
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Oct 01 11:27:58 2025 +0000
@@ -135,15 +135,13 @@
             val filename = "prob_" ^
               StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
               StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+            fun mk_smt_file () = dir ^ "/" ^ filename ^ "__" ^ serial_string ()
           in
             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)
-            #> (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 ())
+            #> (keep_probs ? Config.put SMT_Config.problem_dest_file (mk_smt_file ()))
+            #> (keep_proofs ? Config.put SMT_Config.proof_dest_file (mk_smt_file ()))
           end
         | set_file_name NONE = I
       val state' = state
isabelle