src/HOL/Library/Infinite_Set.thy

--- a/src/HOL/Library/Infinite_Set.thy	Sun Sep 11 22:56:05 2011 +0200
+++ b/src/HOL/Library/Infinite_Set.thy	Mon Sep 12 07:55:43 2011 +0200
@@ -544,7 +544,7 @@
 
 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 (fastforce intro: LeastI dest!: infinite_imp_nonempty)
 apply simp
 apply (metis DiffE infinite_remove)
 done