src/HOL/Tools/Sledgehammer/sledgehammer_run.ML

                 SOME is_app => filter (is_app o prop_of o snd)
               | NONE => I)
           |> relevant_facts ctxt params (hd provers) max_max_facts fact_override
                             hyp_ts concl_t
           |> #1 (*###*)
-          |> map (apfst (apfst (fn name => name ())))
           |> tap (fn facts =>
                      if verbose then
                        label ^ plural_s (length provers) ^ ": " ^
                        (if null facts then
                           "Found no relevant facts."