small improvement in serialization for wfrec
authorhaftmann
Sun Jul 23 07:20:52 2006 +0200 (2006-07-23)
changeset 20185183f08468e19
parent 20184 73b5efaf2aef
child 20186 56207a6f4cc5
small improvement in serialization for wfrec
src/HOL/Wellfounded_Recursion.thy
     1.1 --- a/src/HOL/Wellfounded_Recursion.thy	Sun Jul 23 07:20:26 2006 +0200
     1.2 +++ b/src/HOL/Wellfounded_Recursion.thy	Sun Jul 23 07:20:52 2006 +0200
     1.3 @@ -297,8 +297,8 @@
     1.4  
     1.5  code_constapp
     1.6    wfrec
     1.7 -    ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;")
     1.8 -    haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x")
     1.9 +    ml (target_atom "(let fun wfrec f x = f (wfrec f) x in wfrec end)")
    1.10 +    haskell (target_atom "(wfrec where wfrec f x = f (wfrec f) x)")
    1.11  
    1.12  subsection{*Variants for TFL: the Recdef Package*}
    1.13