--- a/src/HOL/Tools/record_package.ML Sat Oct 13 20:30:38 2001 +0200
+++ b/src/HOL/Tools/record_package.ML Sat Oct 13 20:31:05 2001 +0200
@@ -619,8 +619,8 @@
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 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;
+ |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) field_specs
+ |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) dest_specs;
(* 3rd stage: thms_thy *)
@@ -801,8 +801,8 @@
|> 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 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 (fn x => (x, [Drule.kind_internal]))) sel_specs
+ |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) update_specs
|>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;