| changeset 20185 | 183f08468e19 |
| parent 20105 | 454f4be984b7 |
| child 20435 | d2a30fed7596 |
--- a/src/HOL/Wellfounded_Recursion.thy Sun Jul 23 07:20:26 2006 +0200 +++ b/src/HOL/Wellfounded_Recursion.thy Sun Jul 23 07:20:52 2006 +0200 @@ -297,8 +297,8 @@ code_constapp wfrec - ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;") - haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x") + ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)") + haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)") subsection{*Variants for TFL: the Recdef Package*}