# HG changeset patch
# User haftmann
# Date 1386443375 -3600
# Node ID 0b3a4bdfc3d1a5341377b897841c6ad388fa3c1f
# Parent  d3c656f0b7ab615abc325801929f95b181ece111
default code equations for make, fields, extend and truncate operations on records

diff -r d3c656f0b7ab -r 0b3a4bdfc3d1 src/HOL/Tools/record.ML
--- 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 *)