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