--- 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 *}
--- 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)