no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle

--- a/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 17:32:29 2009 +0200
+++ b/src/HOL/MicroJava/J/TypeRel.thy	Mon Aug 31 20:32:00 2009 +0200
@@ -97,6 +97,14 @@
   qed
 qed
 
+text {* Code generator setup (FIXME!) *}
+
+consts_code
+  "wfrec"   ("\<module>wfrec?")
+attach {*
+fun wfrec f x = f (wfrec f) x;
+*}
+
 consts
 
   method :: "'c prog \<times> cname => ( sig   \<rightharpoonup> cname \<times> ty \<times> 'c)" (* ###curry *)

--- 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 *}