# HG changeset patch
# User berghofe
# Date 1007994903 -3600
# Node ID 95fb2e206dc7730063569da0f924d8d174dc3068
# Parent  473cb9f9e237f2553d616147e77a10d8d31cd82e
Added support for code generation.

diff -r 473cb9f9e237 -r 95fb2e206dc7 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Mon Dec 10 15:34:15 2001 +0100
+++ b/src/HOL/Tools/record_package.ML	Mon Dec 10 15:35:03 2001 +0100
@@ -97,6 +97,14 @@
 
 
 
+(*** code generator data ***)
+
+val [prod_code, fst_code, snd_code] =
+  map (Codegen.parse_mixfix (K (Bound 0))) ["(_,/ _)", "fst", "snd"];
+val prodT_code = Codegen.parse_mixfix (K dummyT) "(_ */ _)";
+
+
+
 (*** syntax operations ***)
 
 (** name components **)
@@ -579,7 +587,6 @@
   let
     val sign = Theory.sign_of thy;
     val base = Sign.base_name;
-    val full_path = Sign.full_name_path sign;
 
     val xT = TFree (variant alphas "'x", HOLogic.typeS);
 
@@ -630,6 +637,12 @@
 
     val (thms_thy, [field_defs', dest_defs', dest_convs', field_injects',
         field_splits', field_inducts', field_cases']) = defs_thy
+      |> Codegen.assoc_consts_i (flat (map (fn (s, _) =>
+           [(suffix fieldN s, None, prod_code),
+            (suffix fstN s, None, fst_code),
+            (suffix sndN s, None, snd_code)]) fields))
+      |> Codegen.assoc_types (map (fn (s, _) =>
+           (suffix field_typeN s, prodT_code)) fields)
       |> (PureThy.add_thmss o map Thm.no_attributes)
        [("field_defs", field_defs),
         ("dest_defs", dest_defs1 @ dest_defs2),