# HG changeset patch
# User desharna
# Date 1637180376 -3600
# Node ID 3094dae0376423e39c8cf73721dd011ebec62f8e
# Parent  db4b8dd587a5e10c9469397a2e383637af26fa80
tuned SMT-Lib file names generated by Mirabelle

diff -r db4b8dd587a5 -r 3094dae03764 src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML
--- a/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Nov 17 19:52:17 2021 +0100
+++ b/src/HOL/Tools/Mirabelle/mirabelle_sledgehammer.ML	Wed Nov 17 21:19:36 2021 +0100
@@ -345,14 +345,15 @@
     val {context = ctxt, facts = chained_ths, goal} = Proof.goal st
     val i = 1
     fun set_file_name (SOME dir) =
-        Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
-        #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix
-          ("prob_" ^
+        let
+          val filename = "prob_" ^
             StringCvt.padLeft #"0" 5 (str0 (Position.line_of pos)) ^ "_" ^
-            StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos)) ^ "__")
-        #> Config.put SMT_Config.debug_files
-          (dir ^ "/" ^ Name.desymbolize (SOME false) (ATP_Util.timestamp ()) ^ "_"
-          ^ serial_string ())
+            StringCvt.padLeft #"0" 6 (str0 (Position.offset_of pos))
+        in
+          Config.put Sledgehammer_Prover_ATP.atp_dest_dir dir
+          #> Config.put Sledgehammer_Prover_ATP.atp_problem_prefix (filename ^ "__")
+          #> Config.put SMT_Config.debug_files (dir ^ "/" ^ filename ^ "__" ^ serial_string ())
+        end
       | set_file_name NONE = I
     val st' =
       st