conceal internal record definitions;
authorwenzelm
Tue Feb 16 13:06:43 2010 +0100 (2010-02-16)
changeset 35142495c623f1e3c
parent 35141 182f27a8716c
child 35143 7b2538c987e7
conceal internal record definitions;
src/HOL/Tools/record.ML
     1.1 --- a/src/HOL/Tools/record.ML	Tue Feb 16 11:59:05 2010 +0100
     1.2 +++ b/src/HOL/Tools/record.ML	Tue Feb 16 13:06:43 2010 +0100
     1.3 @@ -153,7 +153,8 @@
     1.4      val ([isom_def], cdef_thy) =
     1.5        typ_thy
     1.6        |> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
     1.7 -      |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
     1.8 +      |> PureThy.add_defs false
     1.9 +        [Thm.no_attributes (apfst (Binding.conceal o Binding.name) isom_spec)];
    1.10  
    1.11      val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
    1.12      val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
    1.13 @@ -2116,10 +2117,12 @@
    1.14              sel_decls (field_syntax @ [Syntax.NoSyn]))
    1.15        |> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
    1.16            (upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
    1.17 -      |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
    1.18 -      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
    1.19 -      ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
    1.20 -             [make_spec, fields_spec, extend_spec, truncate_spec])
    1.21 +      |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
    1.22 +        sel_specs
    1.23 +      ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
    1.24 +        upd_specs
    1.25 +      ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
    1.26 +        [make_spec, fields_spec, extend_spec, truncate_spec]
    1.27        |->
    1.28          (fn defs as ((sel_defs, upd_defs), derived_defs) =>
    1.29            fold Code.add_default_eqn sel_defs