default code equations for make, fields, extend and truncate operations on records

--- a/src/HOL/Tools/record.ML	Mon Dec 09 21:32:45 2013 +0100
+++ b/src/HOL/Tools/record.ML	Sat Dec 07 20:09:35 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 *)