--- a/src/HOL/Tools/record_package.ML Tue Sep 18 07:36:14 2007 +0200
+++ b/src/HOL/Tools/record_package.ML Tue Sep 18 07:36:15 2007 +0200
@@ -1512,8 +1512,8 @@
||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
|-> (fn args as ((_, dest_defs), upd_defs) =>
- fold (Code.add_func false) dest_defs
- #> fold (Code.add_func false) upd_defs
+ fold Code.add_default_func dest_defs
+ #> fold Code.add_default_func upd_defs
#> pair args);
val ((([abs_inject, abs_inverse, abs_induct], ext_def :: dest_defs), upd_defs), defs_thy) =
timeit_msg "record extension type/selector/update defs:" mk_defs;
@@ -1916,9 +1916,9 @@
||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
[make_spec, fields_spec, extend_spec, truncate_spec])
|-> (fn defs as ((sel_defs, upd_defs), derived_defs) =>
- fold (Code.add_func false) sel_defs
- #> fold (Code.add_func false) upd_defs
- #> fold (Code.add_func false) derived_defs
+ fold Code.add_default_func sel_defs
+ #> fold Code.add_default_func upd_defs
+ #> fold Code.add_default_func derived_defs
#> pair defs)
val (((sel_defs, upd_defs), derived_defs), defs_thy) =
timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"