1.1 --- a/src/HOL/Tools/record.ML	Mon Dec 09 21:32:45 2013 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Sat Dec 07 20:09:35 2013 +0100
     1.3 @@ -2007,7 +2007,8 @@
     1.4            ||>> (Global_Theory.add_defs false o
     1.5                  map (Thm.no_attributes o apfst (Binding.conceal o Binding.name))) upd_specs
     1.6            ||>> (Global_Theory.add_defs false o
     1.7 -                map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
     1.8 +                map (rpair [Code.add_default_eqn_attribute]
     1.9 +                o apfst (Binding.conceal o Binding.name))) (*FIXME Spec_Rules (?)*)
    1.10              [make_spec, fields_spec, extend_spec, truncate_spec]);
    1.11  
    1.12      (* prepare propositions *)