src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML

     val is_blacklisted_or_something = is_blacklisted_or_something ctxt ho_atp
 
     fun add_facts global foldx facts =
       foldx (fn (name0, ths) => fn accum =>
         if name0 <> "" andalso
-           forall (not o member Thm.eq_thm_prop add_ths) ths andalso
-           (Facts.is_concealed facts name0 orelse
-            Long_Name.is_hidden (Facts.intern facts name0) orelse
-            (not generous andalso is_blacklisted_or_something name0)) then
+           (Long_Name.is_hidden (Facts.intern facts name0) orelse
+            ((Facts.is_concealed facts name0 orelse
+              (not generous andalso is_blacklisted_or_something name0)) andalso
+             forall (not o member Thm.eq_thm_prop add_ths) ths)) then
           accum
         else
           let
             val n = length ths
             val multi = n > 1