diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Set.thy	Mon Jul 12 10:48:37 2010 +0200
@@ -1574,7 +1574,7 @@
 subsubsection {* Inverse image of a function *}
 
 definition vimage :: "('a => 'b) => 'b set => 'a set" (infixr "-`" 90) where
-  [code del]: "f -` B == {x. f x : B}"
+  "f -` B == {x. f x : B}"
 
 lemma vimage_eq [simp]: "(a : f -` B) = (f a : B)"
   by (unfold vimage_def) blast
@@ -1657,7 +1657,7 @@
 subsubsection {* Getting the Contents of a Singleton Set *}
 
 definition contents :: "'a set \<Rightarrow> 'a" where
-  [code del]: "contents X = (THE x. X = {x})"
+  "contents X = (THE x. X = {x})"
 
 lemma contents_eq [simp]: "contents {x} = x"
   by (simp add: contents_def)