# HG changeset patch
# User berghofe
# Date 1127754271 -7200
# Node ID 38496187809de819eeea069946635285b43f42c3
# Parent  34c41d9bd749bef0ad03eac9ab4fff55519bc2d5
Renamed wf_rec to wfrec in consts_code declaration.

diff -r 34c41d9bd749 -r 38496187809d src/HOL/Wellfounded_Recursion.thy
--- a/src/HOL/Wellfounded_Recursion.thy	Mon Sep 26 17:14:48 2005 +0200
+++ b/src/HOL/Wellfounded_Recursion.thy	Mon Sep 26 19:04:31 2005 +0200
@@ -283,9 +283,9 @@
 subsection {* Code generator setup *}
 
 consts_code
-  "wfrec"   ("\<module>wf'_rec?")
+  "wfrec"   ("\<module>wfrec?")
 attach {*
-fun wf_rec f x = f (wf_rec f) x;
+fun wfrec f x = f (wfrec f) x;
 *}