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 =