1.1 --- a/src/HOL/TPTP/mash_eval.ML Sat Dec 15 14:45:08 2012 +0100
1.2 +++ b/src/HOL/TPTP/mash_eval.ML Sat Dec 15 18:26:37 2012 +0100
1.3 @@ -88,7 +88,10 @@
1.4 val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
1.5 (* adapted from "mirabelle_sledgehammer.ML" *)
1.6 fun set_file_name heading (SOME dir) =
1.7 - let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
1.8 + let
1.9 + val prob_prefix =
1.10 + "goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading
1.11 + in
1.12 Config.put Sledgehammer_Provers.dest_dir dir
1.13 #> Config.put Sledgehammer_Provers.problem_prefix
1.14 (prob_prefix ^ "__")