# HG changeset patch
# User wenzelm
# Date 1408216268 -7200
# Node ID cb67fac9bd891389b8823667d68de556c6d83089
# Parent  0284a7d083be34ea4655888db434e449929d6f1b
updated to named_theorems;

diff -r 0284a7d083be -r cb67fac9bd89 src/HOL/HOL.thy
--- a/src/HOL/HOL.thy	Sat Aug 16 20:46:59 2014 +0200
+++ b/src/HOL/HOL.thy	Sat Aug 16 21:11:08 2014 +0200
@@ -788,15 +788,7 @@
 seldom-used facts. Some duplicate other rules.
 *}
 
-ML {*
-structure No_ATPs = Named_Thms
-(
-  val name = @{binding no_atp}
-  val description = "theorems that should be filtered out by Sledgehammer"
-)
-*}
-
-setup {* No_ATPs.setup *}
+named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
 
 
 subsubsection {* Classical Reasoner setup *}
diff -r 0284a7d083be -r cb67fac9bd89 src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
--- 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)