src/HOL/Wellfounded_Recursion.thy
changeset 18963 3adfc9dfb30a
parent 18702 7dc7dcd63224
child 19602 e25d1e9a0675
--- a/src/HOL/Wellfounded_Recursion.thy	Mon Feb 06 21:02:01 2006 +0100
+++ b/src/HOL/Wellfounded_Recursion.thy	Tue Feb 07 08:47:43 2006 +0100
@@ -290,10 +290,10 @@
 
 code_primconst wfrec
 ml {*
-fun wfrec f x = f (wfrec f) x;
+fun `_` f x = f (`_` f) x;
 *}
 haskell {*
-wfrec f x = f (wfrec f) x
+`_` f x = f (`_` f) x
 *}
 
 (* code_syntax_const