# HG changeset patch
# User haftmann
# Date 1153632052 -7200
# Node ID 183f08468e192c3fed24745d97d1d205affc25ce
# Parent  73b5efaf2aefac152bdb2d406ec3859e65f394f9
small improvement in serialization for wfrec

diff -r 73b5efaf2aef -r 183f08468e19 src/HOL/Wellfounded_Recursion.thy
--- 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*}