src/HOL/Wellfounded_Recursion.thy

   "wfrec"   ("\<module>wfrec?")
 attach {*
 fun wfrec f x = f (wfrec f) x;
 *}
 
-setup {*
-  CodegenPackage.add_appconst ("Wellfounded_Recursion.wfrec", CodegenPackage.appgen_wfrec)
-*}
-
-code_const wfrec
-  (SML target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
-  (Haskell target_atom "(let wfrec f x = f (wfrec f) x in wfrec)")
 
 subsection{*Variants for TFL: the Recdef Package*}
 
 lemma tfl_wf_induct: "ALL R. wf R -->  
        (ALL P. (ALL x. (ALL y. (y,x):R --> P y) --> P x) --> (ALL x. P x))"