diff -r 95e6eb9044fe -r f4b3f8fbf599 src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Fri Feb 13 09:56:24 2009 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Fri Feb 13 23:55:04 2009 +0100
@@ -461,10 +461,11 @@
   by simp
 
 lemma enumerate_in_set: "infinite S \<Longrightarrow> enumerate S n : S"
-  apply (induct n arbitrary: S)
-   apply (fastsimp intro: LeastI dest!: infinite_imp_nonempty)
-  apply (fastsimp iff: finite_Diff_singleton)
-  done
+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)
+done
 
 declare enumerate_0 [simp del] enumerate_Suc [simp del]