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 #> map fact_of_raw_fact |
114 val find_suggs = |
|
115 find_suggested_facts ctxt facts #> map fact_of_raw_fact |
115 fun get_facts [] compute = compute facts |
116 fun get_facts [] compute = compute facts |
116 | get_facts suggs _ = find_suggs suggs |
117 | get_facts suggs _ = find_suggs suggs |
117 val mepo_facts = |
118 val mepo_facts = |
118 get_facts mepo_suggs (fn _ => |
119 get_facts mepo_suggs (fn _ => |
119 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
120 mepo_suggested_facts ctxt params prover slack_max_facts NONE |
120 hyp_ts concl_t facts) |
121 hyp_ts concl_t facts) |
121 |> weight_mepo_facts |
122 |> weight_mepo_facts |
122 fun mash_of suggs = |
123 fun mash_of suggs = |
123 get_facts suggs (fn _ => |
124 get_facts suggs (fn _ => |
124 find_mash_suggestions slack_max_facts suggs facts [] [] |
125 find_mash_suggestions ctxt slack_max_facts suggs facts [] [] |
125 |> fst |> map fact_of_raw_fact) |
126 |> fst |> map fact_of_raw_fact) |
126 |> weight_mash_facts |
127 |> weight_mash_facts |
127 val mash_isar_facts = mash_of mash_isar_suggs |
128 val mash_isar_facts = mash_of mash_isar_suggs |
128 val mash_prover_facts = mash_of mash_prover_suggs |
129 val mash_prover_facts = mash_of mash_prover_suggs |
129 fun mess_of mash_facts = |
130 fun mess_of mash_facts = |