--- 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.
--- 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 *)