76 val goal = goal_of_thm thy th |
76 val goal = goal_of_thm thy th |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
77 val (_, hyp_ts, concl_t) = ATP_Util.strip_subgoal ctxt goal 1 |
78 val isar_deps = isabelle_dependencies_of all_names th |
78 val isar_deps = isabelle_dependencies_of all_names th |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
79 val facts = facts |> filter (fn (_, th') => thm_ord (th', th) = LESS) |
80 val mepo_facts = |
80 val mepo_facts = |
81 Sledgehammer_Filter_Iter.iterative_relevant_facts ctxt params |
81 Sledgehammer_MePo.iterative_relevant_facts ctxt params prover |
82 prover slack_max_facts NONE hyp_ts concl_t facts |
82 slack_max_facts NONE hyp_ts concl_t facts |
83 val mash_facts = facts |> suggested_facts suggs |
83 val mash_facts = facts |> suggested_facts suggs |
84 val mess = [(mepo_facts, []), (mash_facts, [])] |
84 val mess = [(mepo_facts, []), (mash_facts, [])] |
85 val mesh_facts = mesh_facts slack_max_facts mess |
85 val mesh_facts = mesh_facts slack_max_facts mess |
86 val isar_facts = suggested_facts isar_deps facts |
86 val isar_facts = suggested_facts isar_deps facts |
87 fun prove ok heading facts = |
87 fun prove ok heading facts = |