encode lemma name in file name
authorblanchet
Sat, 15 Dec 2012 18:26:37 +0100
changeset 5157081a1491ba936
parent 51565 8c3c7f158861
child 51571 6209bc89faa3
encode lemma name in file name
src/HOL/TPTP/mash_eval.ML
     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 ^ "__")