src/HOL/Tools/record_package.ML

     (* 2nd stage: defs_thy *)
 
     val (defs_thy, (field_defs, dest_defs)) =
       types_thy
        |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
-       |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) field_specs
-       |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
+       |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) field_specs
+       |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
 
 
     (* 3rd stage: thms_thy *)
 
     val prove = prove_simp (Theory.sign_of defs_thy) HOL_basic_ss;

       |> Theory.add_tyabbrs_i recordT_specs     (*not made part of record name space!*)
       |> Theory.add_path bname
       |> Theory.add_trfuns ([], [], field_tr's, [])
       |> (Theory.add_consts_i o map Syntax.no_syn)
         (sel_decls @ update_decls @ make_decls)
-      |> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) sel_specs
-      |>>> (PureThy.add_defs_i o map (fn x => (x, [Drule.tag_internal]))) update_specs
-      |>>> (PureThy.add_defs_i o map Thm.no_attributes) make_specs;
+      |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) sel_specs
+      |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) update_specs
+      |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;
 
 
     (* 3rd stage: thms_thy *)
 
     val parent_simps = flat (map #simps parents);