# HG changeset patch
# User blanchet
# Date 1355267698 -3600
# Node ID da63f2bc66b37ec782a384078d2d0c3f5a02d5db
# Parent  d7be7ccf428b76a272bdbbedc08aa4aa66fa02db
better name for SMT solver files

diff -r d7be7ccf428b -r da63f2bc66b3 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 00:14:58 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Wed Dec 12 00:14:58 2012 +0100
@@ -90,12 +90,12 @@
         val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
         (* adapted from "mirabelle_sledgehammer.ML" *)
         fun set_file_name heading (SOME dir) =
-            Config.put Sledgehammer_Provers.dest_dir dir
-            #> Config.put Sledgehammer_Provers.problem_prefix
-              ("goal_" ^ string_of_int j ^ "_" ^ heading ^ "__")
-            #> Config.put SMT_Config.debug_files
-              (dir ^ "/" ^ Name.desymbolize false (ATP_Util.timestamp ()) ^ "_"
-              ^ serial_string ())
+            let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
+              Config.put Sledgehammer_Provers.dest_dir dir
+              #> Config.put Sledgehammer_Provers.problem_prefix
+                            (prob_prefix ^ "__")
+              #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
+            end
           | set_file_name _ NONE = I
         fun prove ok heading get facts =
           let