1.1 --- a/src/HOL/Wellfounded_Recursion.thy	Tue Jan 17 10:26:50 2006 +0100
     1.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Tue Jan 17 16:36:57 2006 +0100
     1.3 @@ -288,6 +288,18 @@
     1.4  fun wfrec f x = f (wfrec f) x;
     1.5  *}
     1.6  
     1.7 +code_primconst wfrec
     1.8 +ml {*
     1.9 +fun wfrec f x = f (wfrec f) x;
    1.10 +*}
    1.11 +haskell {*
    1.12 +wfrec f x = f (wfrec f) x
    1.13 +*}
    1.14 +
    1.15 +(* code_syntax_const
    1.16 +  wfrec
    1.17 +    ml ("{*wfrec*}?")
    1.18 +    haskell ("{*wfrec*}?") *)
    1.19  
    1.20  subsection{*Variants for TFL: the Recdef Package*}
    1.21