src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Mon Aug 31 17:32:29 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
@@ -464,14 +464,6 @@
 apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
 done
 
-subsection {* Code generator setup *}
-
-consts_code
-  "wfrec"   ("\<module>wfrec?")
-attach {*
-fun wfrec f x = f (wfrec f) x;
-*}
-
 
 subsection {* @{typ nat} is well-founded *}