diff -r 3e80eab831a1 -r 156925dd67af src/HOL/Library/Infinite_Set.thy
--- a/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:27 2010 +0100
+++ b/src/HOL/Library/Infinite_Set.thy	Sat Jan 16 17:15:28 2010 +0100
@@ -530,11 +530,9 @@
   The set's element type must be wellordered (e.g. the natural numbers).
 *}
 
-consts
-  enumerate   :: "'a::wellorder set => (nat => 'a::wellorder)"
-primrec
-  enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
-  enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
+primrec (in wellorder) enumerate :: "'a set \<Rightarrow> nat \<Rightarrow> 'a" where
+    enumerate_0:   "enumerate S 0       = (LEAST n. n \<in> S)"
+  | enumerate_Suc: "enumerate S (Suc n) = enumerate (S - {LEAST n. n \<in> S}) n"
 
 lemma enumerate_Suc':
     "enumerate S (Suc n) = enumerate (S - {enumerate S 0}) n"