src/HOL/TPTP/mash_eval.ML
changeset 50555 81a1491ba936
parent 50520 f2d33310337a
child 50556 6209bc89faa3
equal deleted inserted replaced
50550:8c3c7f158861 50555:81a1491ba936
    86         val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
    86         val mess = [(0.5, (mepo_facts, [])), (0.5, (mash_facts, mash_unks))]
    87         val mesh_facts = mesh_facts slack_max_facts mess
    87         val mesh_facts = mesh_facts slack_max_facts mess
    88         val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
    88         val isar_facts = find_suggested_facts (map (rpair 1.0) isar_deps) facts
    89         (* adapted from "mirabelle_sledgehammer.ML" *)
    89         (* adapted from "mirabelle_sledgehammer.ML" *)
    90         fun set_file_name heading (SOME dir) =
    90         fun set_file_name heading (SOME dir) =
    91             let val prob_prefix = "goal_" ^ string_of_int j ^ "_" ^ heading in
    91             let
       
    92               val prob_prefix =
       
    93                 "goal_" ^ string_of_int j ^ "__" ^ name ^ "__" ^ heading
       
    94             in
    92               Config.put Sledgehammer_Provers.dest_dir dir
    95               Config.put Sledgehammer_Provers.dest_dir dir
    93               #> Config.put Sledgehammer_Provers.problem_prefix
    96               #> Config.put Sledgehammer_Provers.problem_prefix
    94                             (prob_prefix ^ "__")
    97                             (prob_prefix ^ "__")
    95               #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
    98               #> Config.put SMT_Config.debug_files (dir ^ "/" ^ prob_prefix)
    96             end
    99             end