Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 57963 cb67fac9bd89
parent 57729 2df9ed24114f
child 57983 6edc3529bb4e 
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Aug 16 20:46:59 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Aug 16 21:11:08 2014 +0200
@@ -536,7 +536,8 @@
            val facts =
              all_facts ctxt false ho_atp reserved add chained css
              |> filter_out ((member Thm.eq_thm_prop del orf
-               (No_ATPs.member ctxt andf not o member Thm.eq_thm_prop add)) o snd)
+               (Named_Theorems.member ctxt @{named_theorems no_atp} andf
+                 not o member Thm.eq_thm_prop add)) o snd)
          in
            facts
          end)
isabelle