Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
removed completely needless, inefficient code
authorblanchet
Tue, 10 Sep 2013 15:56:51 +0200
changeset 53510 c0982ad1281d
parent 53509 cf7679195169
child 53511 3ea6b9461c55
removed completely needless, inefficient code
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML file | annotate | diff | comparison | revisions 
--- 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
isabelle