updated to named_theorems;
authorwenzelm
Sat Aug 16 21:11:08 2014 +0200 (2014-08-16)
changeset 57963cb67fac9bd89
parent 57962 0284a7d083be
child 57964 3dfc1bf3ac3d
updated to named_theorems;
src/HOL/HOL.thy
src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
     1.1 --- a/src/HOL/HOL.thy	Sat Aug 16 20:46:59 2014 +0200
     1.2 +++ b/src/HOL/HOL.thy	Sat Aug 16 21:11:08 2014 +0200
     1.3 @@ -788,15 +788,7 @@
     1.4  seldom-used facts. Some duplicate other rules.
     1.5  *}
     1.6  
     1.7 -ML {*
     1.8 -structure No_ATPs = Named_Thms
     1.9 -(
    1.10 -  val name = @{binding no_atp}
    1.11 -  val description = "theorems that should be filtered out by Sledgehammer"
    1.12 -)
    1.13 -*}
    1.14 -
    1.15 -setup {* No_ATPs.setup *}
    1.16 +named_theorems no_atp "theorems that should be filtered out by Sledgehammer"
    1.17  
    1.18  
    1.19  subsubsection {* Classical Reasoner setup *}
     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Aug 16 20:46:59 2014 +0200
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Sat Aug 16 21:11:08 2014 +0200
     2.3 @@ -536,7 +536,8 @@
     2.4             val facts =
     2.5               all_facts ctxt false ho_atp reserved add chained css
     2.6               |> filter_out ((member Thm.eq_thm_prop del orf
     2.7 -               (No_ATPs.member ctxt andf not o member Thm.eq_thm_prop add)) o snd)
     2.8 +               (Named_Theorems.member ctxt @{named_theorems no_atp} andf
     2.9 +                 not o member Thm.eq_thm_prop add)) o snd)
    2.10           in
    2.11             facts
    2.12           end)