# HG changeset patch
# User haftmann
# Date 1177060909 -7200
# Node ID 0c9c413b467818d9710e7eff5c7b1f53dc33a7d5
# Parent  f090ecd44f12066bf344bee3940a978ad5bbfd47
add definitions explicitly to code generator table

diff -r f090ecd44f12 -r 0c9c413b4678 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Fri Apr 20 11:21:48 2007 +0200
+++ b/src/HOL/Tools/record_package.ML	Fri Apr 20 11:21:49 2007 +0200
@@ -1506,15 +1506,17 @@
     (* 1st stage: defs_thy *)
     fun mk_defs () =
       thy
-        |> extension_typedef name repT (alphas@[zeta])
-        ||> Theory.add_consts_i
-              (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
-        ||>> PureThy.add_defs_i false (map Thm.no_attributes (ext_spec::dest_specs))
-        ||>> PureThy.add_defs_i false (map Thm.no_attributes upd_specs)
-        |> swap
-    val (defs_thy, (([abs_inject, abs_inverse, abs_induct],ext_def::dest_defs),upd_defs)) =
-        timeit_msg "record extension type/selector/update defs:" mk_defs;
-
+      |> extension_typedef name repT (alphas@[zeta])
+      ||> Theory.add_consts_i
+            (map Syntax.no_syn ((apfst base ext_decl)::dest_decls@upd_decls))
+      ||>> 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 (CodegenData.add_func false) dest_defs
+          #> fold (CodegenData.add_func false) 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;
 
     (* prepare propositions *)
     val _ = timing_msg "record extension preparing propositions";
@@ -1898,25 +1900,29 @@
 
     fun mk_defs () =
       extension_thy
-        |> Theory.add_trfuns
-            ([],[],field_tr's, [])
-        |> Theory.add_advanced_trfuns
-            ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
-        |> Theory.parent_path
-        |> Theory.add_tyabbrs_i recordT_specs
-        |> Theory.add_path bname
-        |> Theory.add_consts_i
-            (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
-        |> (Theory.add_consts_i o map Syntax.no_syn)
-            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
-        |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
-        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
-        ||>> ((PureThy.add_defs_i false o map Thm.no_attributes)
-               [make_spec, fields_spec, extend_spec, truncate_spec])
-        |> swap
-    val (defs_thy,((sel_defs,upd_defs),derived_defs)) =
-        timeit_msg "record trfuns/tyabbrs/selectors/updates/make/fields/extend/truncate defs:"
-         mk_defs;
+      |> Theory.add_trfuns
+          ([],[],field_tr's, [])
+      |> Theory.add_advanced_trfuns
+          ([],[],adv_ext_tr's @ adv_record_type_tr's @ adv_record_type_abbr_tr's,[])
+      |> Theory.parent_path
+      |> Theory.add_tyabbrs_i recordT_specs
+      |> Theory.add_path bname
+      |> Theory.add_consts_i
+          (map2 (fn (x, T) => fn mx => (x, T, mx)) sel_decls (field_syntax @ [Syntax.NoSyn]))
+      |> (Theory.add_consts_i o map Syntax.no_syn)
+          (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
+      |> ((PureThy.add_defs_i false o map Thm.no_attributes) sel_specs)
+      ||>> ((PureThy.add_defs_i false o map Thm.no_attributes) upd_specs)
+      ||>> ((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 (CodegenData.add_func false) sel_defs
+          #> fold (CodegenData.add_func false) upd_defs
+          #> fold (CodegenData.add_func false) 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:"
+        mk_defs;
 
 
     (* prepare propositions *)