# HG changeset patch
# User wenzelm
# Date 1386627370 -3600
# Node ID afdb394ee0c03771bce773d19e47c0b695936cad
# Parent  8e71c6ed4d747bf419b32d86e73e71407f45fa4f# Parent  87402674fe2f01288416b1f558b0282c3dfe1134
merged

diff -r 87402674fe2f -r afdb394ee0c0 NEWS
--- a/NEWS	Mon Dec 09 22:02:42 2013 +0100
+++ b/NEWS	Mon Dec 09 23:16:10 2013 +0100
@@ -24,6 +24,9 @@
 
 *** HOL ***
 
+* Code generations are provided for make, fields, extend and truncate
+operations on records.
+
 * Qualified constant names Wellfounded.acc, Wellfounded.accp.
 INCOMPATIBILITY.
 
diff -r 87402674fe2f -r afdb394ee0c0 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Dec 09 22:02:42 2013 +0100
+++ b/src/HOL/Tools/record.ML	Mon Dec 09 23:16:10 2013 +0100
@@ -2007,7 +2007,8 @@
           ||>> (Global_Theory.add_defs false o
                 map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
           ||>> (Global_Theory.add_defs false o
-                map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+                map (rpair [Code.add_default_eqn_attribute]
+                o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
             [make_spec, fields_spec, extend_spec, truncate_spec]);
 
     (* prepare propositions *)