src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

     fun add_facts global foldx facts =
       foldx (fn (name0, ths) =>
         if name0 <> "" andalso
            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
            (Facts.is_concealed facts name0 orelse
-            not (can (Proof_Context.get_thms ctxt) name0) orelse
             (not generous andalso
              is_blacklisted_or_something ctxt ho_atp name0)) then
           I
         else
           let