--- 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]