--- a/src/HOL/Tools/recfun_codegen.ML Fri Aug 10 17:04:24 2007 +0200
+++ b/src/HOL/Tools/recfun_codegen.ML Fri Aug 10 17:04:34 2007 +0200
@@ -44,7 +44,7 @@
handle TERM _ => tap (fn _ => warn thm);
in
Thm.declaration_attribute (fn thm => Context.mapping
- (add thm #> CodegenData.add_func false thm) I)
+ (add thm #> Code.add_func false thm) I)
end;
fun del_thm thm thy =
@@ -58,7 +58,7 @@
end handle TERM _ => (warn thm; thy);
val del = Thm.declaration_attribute
- (fn thm => Context.mapping (del_thm thm #> CodegenData.del_func thm) I)
+ (fn thm => Context.mapping (del_thm thm #> Code.del_func thm) I)
fun del_redundant thy eqs [] = eqs
| del_redundant thy eqs (eq :: eqs') =
@@ -170,9 +170,8 @@
val setup =
- add_codegen "recfun" recfun_codegen #>
- add_attribute ""
- (Args.del |-- Scan.succeed del
+ add_codegen "recfun" recfun_codegen
+ #> Code.add_attribute ("", Args.del |-- Scan.succeed del
|| Scan.option (Args.$$$ "target" |-- Args.colon |-- Args.name) >> add);
end;