diff -r c02b0c727780 -r 2bc5b5cf0516 src/HOL/Tools/record_package.ML
--- a/src/HOL/Tools/record_package.ML	Wed Jul 29 15:38:08 1998 +0200
+++ b/src/HOL/Tools/record_package.ML	Thu Jul 30 15:24:59 1998 +0200
@@ -593,7 +593,8 @@
       |> (Theory.add_consts_i o map Syntax.no_syn)
         (sel_decls @ update_decls @ make_decls)
       |> (PureThy.add_defs_i o map (fn x => (x, [Attribute.tag_internal])))
-        (sel_specs @ update_specs @ make_specs);
+        (sel_specs @ update_specs)
+      |> (PureThy.add_defs_i o map Attribute.none) make_specs;
 
     val sel_defs = get_defs defs_thy sel_specs;
     val update_defs = get_defs defs_thy update_specs;