# HG changeset patch
# User desharna
# Date 1637181373 -3600
# Node ID dacd9a08f0a34ee1b7321dbd8fa4bf54926e706c
# Parent  3094dae0376423e39c8cf73721dd011ebec62f8e
tuned TPTP file names generated by Sledgehammer

diff -r 3094dae03764 -r dacd9a08f0a3 src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Nov 17 21:19:36 2021 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML	Wed Nov 17 21:36:13 2021 +0100
@@ -151,6 +151,7 @@
     val problem_file_name =
       Path.basic (problem_prefix ^ (if overlord then "" else serial_string ()) ^
         suffix_of_mode mode ^ "_" ^ string_of_int subgoal)
+      |> Path.ext "p"
     val prob_path =
       if dest_dir = "" then
         File.tmp_path problem_file_name
@@ -342,8 +343,16 @@
        the proof file too. *)
     fun clean_up () = if dest_dir = "" then (try File.rm prob_path; ()) else ()
     fun export (_, (output, _, _, _, _), _) =
-      if dest_dir = "" then ()
-      else File.write (Path.explode (Path.implode prob_path ^ "_proof")) output
+      let
+        val make_export_path =
+          Path.split_ext
+          #> apfst (Path.explode o suffix "_proof" o Path.implode)
+          #> swap
+          #> uncurry Path.ext
+      in
+        if dest_dir = "" then ()
+        else File.write (make_export_path prob_path) output
+      end
 
     val ((_, (_, pool, lifted, sym_tab)), (output, run_time, used_from, atp_proof, outcome),
          SOME (format, type_enc)) =