src/HOL/Wellfounded.thy
changeset 32461 eee4fa79398f
parent 32263 8bc0fd4a23a0
child 32462 c33faa289520
     1.1 --- a/src/HOL/Wellfounded.thy	Mon Aug 31 17:32:29 2009 +0200
     1.2 +++ b/src/HOL/Wellfounded.thy	Mon Aug 31 20:32:00 2009 +0200
     1.3 @@ -464,14 +464,6 @@
     1.4  apply (erule adm_lemma [THEN wfrec_unique, THEN theI'])
     1.5  done
     1.6  
     1.7 -subsection {* Code generator setup *}
     1.8 -
     1.9 -consts_code
    1.10 -  "wfrec"   ("\<module>wfrec?")
    1.11 -attach {*
    1.12 -fun wfrec f x = f (wfrec f) x;
    1.13 -*}
    1.14 -
    1.15  
    1.16  subsection {* @{typ nat} is well-founded *}
    1.17