# HG changeset patch
# User krauss
# Date 1251743520 -7200
# Node ID eee4fa79398faceda6c9de752ca9c09830726e8a
# Parent  ba0cf920a39c3d4766508ab26289e2e9039cc8f0
no consts_code for wfrec, as it violates the "code generation = equational reasoning" principle

diff -r ba0cf920a39c -r eee4fa79398f src/HOL/MicroJava/J/TypeRel.thy
--- 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 *)
diff -r ba0cf920a39c -r eee4fa79398f 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 *}