# HG changeset patch
# User haftmann
# Date 1147162257 -7200
# Node ID e25d1e9a06754db792e0d5bd796a07e83624c122
# Parent  299d4cd2ef518604a16ca7bbf6432c26d458f1fe
improved code generation for wfrec

diff -r 299d4cd2ef51 -r e25d1e9a0675 src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Tue May 09 10:10:28 2006 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue May 09 10:10:57 2006 +0200
@@ -288,18 +288,14 @@
 fun wfrec f x = f (wfrec f) x;
 *}
 
-code_primconst wfrec
-ml {*
-fun `_` f x = f (`_` f) x;
-*}
-haskell {*
-`_` f x = f (`_` f) x
+setup {*
+  CodegenPackage.add_appconst ("wfrec", ((3, 3), CodegenPackage.appgen_wfrec))
 *}
 
-(* code_syntax_const
+code_syntax_const
   wfrec
-    ml ("{*wfrec*}?")
-    haskell ("{*wfrec*}?") *)
+    ml ("let fun wfrec f x = f (wfrec f) x in wfrec _ _ end;")
+    haskell ("wfrec _ _ where wfrec f x = f (wfrec f) x")
 
 subsection{*Variants for TFL: the Recdef Package*}