# HG changeset patch
# User wenzelm
# Date 1002997865 -7200
# Node ID c0ca4b89159c2005375825228486d4714de9367a
# Parent  7c7a902a5c651b7935e9fd88ad9eead5e16b3060
Drule.tag_internal;

diff -r 7c7a902a5c65 -r c0ca4b89159c src/HOL/Tools/record_package.ML
--- 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;