src/HOL/Finite_Set.thy

--- a/src/HOL/Finite_Set.thy	Fri Nov 23 21:09:30 2007 +0100
+++ b/src/HOL/Finite_Set.thy	Fri Nov 23 21:09:32 2007 +0100
@@ -1500,9 +1500,10 @@
 But now that we have @{text setsum} things are easy:
 *}
 
-constdefs
-  card :: "'a set => nat"
-  "card A == setsum (%x. 1::nat) A"
+definition
+  card :: "'a set \<Rightarrow> nat"
+where
+  [code func del]: "card A = setsum (\<lambda>x. 1) A"
 
 lemma card_empty [simp]: "card {} = 0"
 by (simp add: card_def)