# HG changeset patch
# User blanchet
# Date 1355592397 -3600
# Node ID 81a1491ba936967aaa9a29565540ad0e1ba65ba5
# Parent  8c3c7f1588614f6d13bfb9a042f6c6f602e3f475
encode lemma name in file name

diff -r 8c3c7f158861 -r 81a1491ba936 src/HOL/TPTP/mash_eval.ML
--- a/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 14:45:08 2012 +0100
+++ b/src/HOL/TPTP/mash_eval.ML	Sat Dec 15 18:26:37 2012 +0100
@@ -88,7 +88,10 @@
         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) =
-            let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
+            let
+              val prob_prefix =
+                "goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading
+            in
               Config.put Sledgehammer_Provers.dest_dir dir
               #> Config.put Sledgehammer_Provers.problem_prefix
                             (prob_prefix ^ "__")