src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Fri Aug 12 07:13:12 2011 -0700
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Aug 12 07:18:28 2011 -0700
@@ -546,7 +546,7 @@
 apply (induct n arbitrary: S)
  apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
 apply simp
-apply (metis Collect_def Collect_mem_eq DiffE infinite_remove)
+apply (metis Collect_mem_eq DiffE infinite_remove)
 done
 
 declare enumerate_0 [simp del] enumerate_Suc [simp del]