src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 16:49:45 2011 -0700
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Aug 22 17:22:49 2011 -0700
@@ -546,7 +546,7 @@
 apply (induct n arbitrary: S)
  apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
 apply simp
-apply (metis Collect_mem_eq DiffE infinite_remove)
+apply (metis DiffE infinite_remove)
 done
 
 declare enumerate_0 [simp del] enumerate_Suc [simp del]