# HG changeset patch
# User haftmann
# Date 1147162212 -7200
# Node ID 2d969d9a233bcfe7288a1aeb88b01553f7e83c56
# Parent  a5c7eb37d14f18a094b5d0b9a381eb2b5f9341db
adaption to CodegenTheorems

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') =