removed completely needless, inefficient code
authorblanchet
Tue Sep 10 15:56:51 2013 +0200 (2013-09-10 ago)
changeset 53510c0982ad1281d
parent 53509 cf7679195169
child 53511 3ea6b9461c55
removed completely needless, inefficient code
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     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