src/HOL/TPTP/mash_eval.ML
changeset 50967 00d87ade2294
parent 50965 7a7d1418301e
child 51004 5f2788c38127
equal deleted inserted replaced
50966:b85cb3049df9 50967:00d87ade2294
   109             | NONE => error ("No fact called \"" ^ name ^ "\".")
   109             | NONE => error ("No fact called \"" ^ name ^ "\".")
   110           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
   110           val goal = goal_of_thm (Proof_Context.theory_of ctxt) th
   111           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   111           val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1
   112           val isar_deps = isar_dependencies_of name_tabs th
   112           val isar_deps = isar_dependencies_of name_tabs th
   113           val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
   113           val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS)
       
   114           val find_suggs = find_suggested_facts facts
   114           fun get_facts [] compute = compute facts
   115           fun get_facts [] compute = compute facts
   115             | get_facts suggs _ = find_suggested_facts suggs facts
   116             | get_facts suggs _ = find_suggs suggs
   116           val mepo_facts =
   117           val mepo_facts =
   117             get_facts mepo_suggs (fn _ =>
   118             get_facts mepo_suggs (fn _ =>
   118                 mepo_suggested_facts ctxt params prover slack_max_facts NONE
   119                 mepo_suggested_facts ctxt params prover slack_max_facts NONE
   119                                      hyp_ts concl_t facts)
   120                                      hyp_ts concl_t facts)
   120             |> weight_mepo_facts
   121             |> weight_mepo_facts
   131             get_facts suggs (fn _ =>
   132             get_facts suggs (fn _ =>
   132                 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
   133                 mesh_facts (Thm.eq_thm_prop o pairself snd) slack_max_facts
   133                            (mess_of mash_facts))
   134                            (mess_of mash_facts))
   134           val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
   135           val mesh_isar_facts = mesh_of mesh_isar_suggs mash_isar_facts
   135           val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
   136           val mesh_prover_facts = mesh_of mesh_prover_suggs mash_prover_facts
   136           val isar_facts = find_suggested_facts isar_deps facts
   137           val isar_facts = find_suggs isar_deps
   137           (* adapted from "mirabelle_sledgehammer.ML" *)
   138           (* adapted from "mirabelle_sledgehammer.ML" *)
   138           fun set_file_name method (SOME dir) =
   139           fun set_file_name method (SOME dir) =
   139               let
   140               let
   140                 val prob_prefix =
   141                 val prob_prefix =
   141                   "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^
   142                   "goal_" ^ string_of_int j ^ "__" ^ encode_str name ^ "__" ^