src/HOL/Library/Infinite_Set.thy

     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"
   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 (fastforce intro: LeastI dest!: infinite_imp_nonempty)
 apply simp
 apply (metis DiffE infinite_remove)
 done
 
 declare enumerate_0 [simp del] enumerate_Suc [simp del]