diff -r a779f463bae4 -r a2b7a20d6ea3 src/HOL/Recdef.thy
--- a/src/HOL/Recdef.thy	Mon Jul 12 08:58:27 2010 +0200
+++ b/src/HOL/Recdef.thy	Mon Jul 12 10:48:37 2010 +0200
@@ -38,7 +38,7 @@
 
 definition
   wfrec :: "('a * 'a) set => (('a => 'b) => 'a => 'b) => 'a => 'b" where
-  [code del]: "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
+  "wfrec R F == %x. THE y. wfrec_rel R (%f x. F (cut f R x) x) x y"
 
 subsection{*Well-Founded Recursion*}