src/HOL/Wellfounded_Recursion.thy

 text{** This form avoids giant explosions in proofs.  NOTE USE OF ==*}
 lemma def_wfrec: "[| f==wfrec r H;  wf(r) |] ==> f(a) = H (cut f r a) a"
 apply auto
 apply (blast intro: wfrec)
 done
+
+
+subsection {* Code generator setup *}
+
+consts_code
+  "wfrec"   ("\<module>wf'_rec?")
+attach {*
+fun wf_rec f x = f (wf_rec f) x;
+*}
 
 
 subsection{*Variants for TFL: the Recdef Package*}
 
 lemma tfl_wf_induct: "ALL R. wf R -->