diff -r d6ecc5828b14 -r 3adfc9dfb30a src/HOL/Wellfounded_Recursion.thy
--- 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