code lemma for contents

--- a/src/HOL/Set.thy	Thu Jul 19 21:47:43 2007 +0200
+++ b/src/HOL/Set.thy	Thu Jul 19 21:47:44 2007 +0200
@@ -2105,9 +2105,10 @@
 
 constdefs
   contents :: "'a set => 'a"
-   "contents X == THE x. X = {x}"
-
-lemma contents_eq [simp]: "contents {x} = x"
+  "contents X == THE x. X = {x}"
+lemmas [code func del] = contents_def
+
+lemma contents_eq [simp, code func]: "contents {x} = x"
 by (simp add: contents_def)