--- a/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 15:13:52 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_filter.ML Wed Dec 15 16:42:06 2010 +0100
@@ -539,10 +539,8 @@
relevant [] [] hopeful
end
fun add_facts ths accepts =
- (facts |> filter ((member Thm.eq_thm ths
- andf (not o member (Thm.eq_thm o apsnd snd) accepts))
- o snd))
- @ accepts
+ (facts |> filter (member Thm.eq_thm ths o snd)) @
+ (accepts |> filter_out (member Thm.eq_thm ths o snd))
|> take max_relevant
in
facts |> map_filter (pair_consts_fact thy is_built_in_const fudge)