equal
deleted
inserted
replaced
134 hyp_ts concl_t |
134 hyp_ts concl_t |
135 |> filter (is_appropriate_prop o prop_of o snd) |
135 |> filter (is_appropriate_prop o prop_of o snd) |
136 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params |
136 |> Sledgehammer_MePo.mepo_suggested_facts ctxt params |
137 default_prover (the_default default_max_facts max_facts) |
137 default_prover (the_default default_max_facts max_facts) |
138 (SOME relevance_fudge) hyp_ts concl_t |
138 (SOME relevance_fudge) hyp_ts concl_t |
139 |> map ((fn name => name ()) o fst o fst) |
139 |> map (fst o fst) |
140 val (found_facts, lost_facts) = |
140 val (found_facts, lost_facts) = |
141 flat proofs |> sort_distinct string_ord |
141 flat proofs |> sort_distinct string_ord |
142 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
142 |> map (fn fact => (find_index (curry (op =) fact) facts, fact)) |
143 |> List.partition (curry (op <=) 0 o fst) |
143 |> List.partition (curry (op <=) 0 o fst) |
144 |>> sort (prod_ord int_ord string_ord) ||> map snd |
144 |>> sort (prod_ord int_ord string_ord) ||> map snd |