author | haftmann |
Sun, 23 Jul 2006 07:20:52 +0200 (2006-07-23) | |
changeset 20185 | 183f08468e19 |
parent 20184 | 73b5efaf2aef |
child 20186 | 56207a6f4cc5 |
--- 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*}