src/HOL/Tools/recfun_codegen.ML
changeset 22484 25dfebd7b4c8
parent 22360 26ead7ed4f4b
child 22846 fb79144af9a3
--- a/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:40 2007 +0100
+++ b/src/HOL/Tools/recfun_codegen.ML	Tue Mar 20 15:52:41 2007 +0100
@@ -46,7 +46,7 @@
       handle TERM _ => tap (fn _ => warn thm);
   in
     Thm.declaration_attribute (fn thm => Context.mapping
-      (add thm #> CodegenData.add_func_legacy thm) I)
+      (add thm #> CodegenData.add_func false thm) I)
   end;
 
 fun del_thm thm thy =