"no_atp" fact that leads to unsound proofs

--- a/src/HOL/Set.thy	Mon Aug 23 11:56:30 2010 +0200
+++ b/src/HOL/Set.thy	Mon Aug 23 12:13:58 2010 +0200
@@ -495,7 +495,7 @@
   apply (rule Collect_mem_eq)
   done
 
-lemma expand_set_eq: "(A = B) = (ALL x. (x:A) = (x:B))"
+lemma expand_set_eq [no_atp]: "(A = B) = (ALL x. (x:A) = (x:B))"
 by(auto intro:set_ext)
 
 lemma subset_antisym [intro!]: "A \<subseteq> B ==> B \<subseteq> A ==> A = B"