# HG changeset patch
# User blanchet
# Date 1378821411 -7200
# Node ID c0982ad1281d9c797af80f545a4d0a77ba25891b
# Parent  cf7679195169c9a67bfd605d086bce72b289cc8a
removed completely needless, inefficient code

diff -r cf7679195169 -r c0982ad1281d src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Tue Sep 10 15:56:51 2013 +0200
@@ -448,7 +448,6 @@
         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