diff -r bafb24c150c1 -r c0401da7726d src/HOL/Infinite_Set.thy
--- a/src/HOL/Infinite_Set.thy	Fri May 21 21:14:18 2004 +0200
+++ b/src/HOL/Infinite_Set.thy	Fri May 21 21:14:52 2004 +0200
@@ -245,8 +245,8 @@
   assumes inf: "infinite (S::'a set)"
   shows "\<exists>f. inj (f::nat \<Rightarrow> 'a) \<and> range f \<subseteq> S"
 proof -
-  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {\<epsilon> e. e \<in> T})"
-  def pick \<equiv> "\<lambda>n. (\<epsilon> e. e \<in> Sseq n)"
+  def Sseq \<equiv> "nat_rec S (\<lambda>n T. T - {SOME e. e \<in> T})"
+  def pick \<equiv> "\<lambda>n. (SOME e. e \<in> Sseq n)"
   have Sseq_inf: "\<And>n. infinite (Sseq n)"
   proof -
     fix n