src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML
changeset 54143 18def1c73c79
parent 54142 5f3c1b445253
child 54503 b490e15a5e19
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Thu Oct 17 23:41:00 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_fact.ML	Fri Oct 18 00:05:31 2013 +0200
     1.3 @@ -544,7 +544,8 @@
     1.4             val (add, del) = pairself (Attrib.eval_thms ctxt) (add, del)
     1.5             val facts =
     1.6               all_facts ctxt false ho_atp reserved add chained css
     1.7 -             |> filter_out ((member Thm.eq_thm_prop del orf No_ATPs.member ctxt) o snd)
     1.8 +             |> filter_out ((member Thm.eq_thm_prop del orf
     1.9 +               (No_ATPs.member ctxt andf not o member Thm.eq_thm_prop add)) o snd)
    1.10           in
    1.11             facts
    1.12           end)