diff -r a5c7eb37d14f -r 2d969d9a233b src/HOL/Tools/recfun_codegen.ML
--- a/src/HOL/Tools/recfun_codegen.ML	Tue May 09 10:09:37 2006 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue May 09 10:10:12 2006 +0200
@@ -61,7 +61,7 @@
   end handle TERM _ => (warn thm; thy);
 
 val del = Thm.declaration_attribute
-  (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_def thm))
+  (fn thm => Context.map_theory (del_thm thm #> CodegenTheorems.del_fun thm))
 
 fun del_redundant thy eqs [] = eqs
   | del_redundant thy eqs (eq :: eqs') =