Drule.tag_internal;
authorwenzelm
Sat Oct 13 20:31:05 2001 +0200 (2001-10-13)
changeset 11739c0ca4b89159c
parent 11738 7c7a902a5c65
child 11740 86ac4189a1c1
Drule.tag_internal;
src/HOL/Tools/record_package.ML
     1.1 --- a/src/HOL/Tools/record_package.ML	Sat Oct 13 20:30:38 2001 +0200
     1.2 +++ b/src/HOL/Tools/record_package.ML	Sat Oct 13 20:31:05 2001 +0200
     1.3 @@ -619,8 +619,8 @@
     1.4      val (defs_thy, (field_defs, dest_defs)) =
     1.5        types_thy
     1.6         |> (Theory.add_consts_i o map (Syntax.no_syn o apfst base)) (field_decls @ dest_decls)
     1.7 -       |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) field_specs
     1.8 -       |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) dest_specs;
     1.9 +       |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) field_specs
    1.10 +       |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) dest_specs;
    1.11  
    1.12  
    1.13      (* 3rd stage: thms_thy *)
    1.14 @@ -801,8 +801,8 @@
    1.15        |> Theory.add_trfuns ([], [], field_tr's, [])
    1.16        |> (Theory.add_consts_i o map Syntax.no_syn)
    1.17          (sel_decls @ update_decls @ make_decls)
    1.18 -      |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) sel_specs
    1.19 -      |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.tag_internal]))) update_specs
    1.20 +      |> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) sel_specs
    1.21 +      |>>> (PureThy.add_defs_i false o map (fn x => (x, [Drule.kind_internal]))) update_specs
    1.22        |>>> (PureThy.add_defs_i false o map Thm.no_attributes) make_specs;
    1.23  
    1.24