src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 53510 c0982ad1281d
parent 53509 cf7679195169
child 53511 3ea6b9461c55
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
     1.3 @@ -448,7 +448,6 @@
     1.4          if name0 <> "" andalso
     1.5             forall (not o member Thm.eq_thm_prop add_ths) ths andalso
     1.6             (Facts.is_concealed facts name0 orelse
     1.7 -            not (can (Proof_Context.get_thms ctxt) name0) orelse
     1.8              (not generous andalso
     1.9               is_blacklisted_or_something ctxt ho_atp name0)) then
    1.10            I