src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 53510 c0982ad1281d
parent 53509 cf7679195169
child 53511 3ea6b9461c55
equal deleted inserted replaced
53509:cf7679195169 53510:c0982ad1281d
   446     fun add_facts global foldx facts =
   446     fun add_facts global foldx facts =
   447       foldx (fn (name0, ths) =>
   447       foldx (fn (name0, ths) =>
   448         if name0 <> "" andalso
   448         if name0 <> "" andalso
   449            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   449            forall (not o member Thm.eq_thm_prop add_ths) ths andalso
   450            (Facts.is_concealed facts name0 orelse
   450            (Facts.is_concealed facts name0 orelse
   451             not (can (Proof_Context.get_thms ctxt) name0) orelse
       
   452             (not generous andalso
   451             (not generous andalso
   453              is_blacklisted_or_something ctxt ho_atp name0)) then
   452              is_blacklisted_or_something ctxt ho_atp name0)) then
   454           I
   453           I
   455         else
   454         else
   456           let
   455           let