--- a/src/HOL/Tools/record.ML Tue Feb 16 11:59:05 2010 +0100
+++ b/src/HOL/Tools/record.ML Tue Feb 16 13:06:43 2010 +0100
@@ -153,7 +153,8 @@
val ([isom_def], cdef_thy) =
typ_thy
|> Sign.add_consts_i [Syntax.no_syn (isom_bind, isomT)]
- |> PureThy.add_defs false [Thm.no_attributes (apfst Binding.name isom_spec)];
+ |> PureThy.add_defs false
+ [Thm.no_attributes (apfst (Binding.conceal o Binding.name) isom_spec)];
val iso_tuple = isom_def RS (abs_inverse RS (rep_inject RS iso_tuple_intro));
val cons = Const (@{const_name iso_tuple_cons}, isomT --> leftT --> rightT --> absT);
@@ -2116,10 +2117,12 @@
sel_decls (field_syntax @ [Syntax.NoSyn]))
|> (Sign.add_consts_i o map (fn (x, T) => (Binding.name x, T, Syntax.NoSyn)))
(upd_decls @ [make_decl, fields_decl, extend_decl, truncate_decl])
- |> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) sel_specs)
- ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name)) upd_specs)
- ||>> ((PureThy.add_defs false o map (Thm.no_attributes o apfst Binding.name))
- [make_spec, fields_spec, extend_spec, truncate_spec])
+ |> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+ sel_specs
+ ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+ upd_specs
+ ||>> (PureThy.add_defs false o map (Thm.no_attributes o apfst (Binding.conceal o Binding.name)))
+ [make_spec, fields_spec, extend_spec, truncate_spec]
|->
(fn defs as ((sel_defs, upd_defs), derived_defs) =>
fold Code.add_default_eqn sel_defs