--- 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 ^ "__")