src/HOL/Mirabelle/Tools/mirabelle_sledgehammer_filter.ML

                hyp_ts concl_t
            |> filter (is_appropriate_prop o prop_of o snd)
            |> Sledgehammer_MePo.mepo_suggested_facts ctxt params
                   default_prover (the_default default_max_facts max_facts)
                   (SOME relevance_fudge) hyp_ts concl_t
-            |> map ((fn name => name ()) o fst o fst)
+            |> map (fst o fst)
          val (found_facts, lost_facts) =
            flat proofs |> sort_distinct string_ord
            |> map (fn fact => (find_index (curry (op =) fact) facts, fact))
            |> List.partition (curry (op <=) 0 o fst)
            |>> sort (prod_ord int_ord string_ord) ||> map snd