# HG changeset patch
# User krauss
# Date 1257197037 -3600
# Node ID 2240b0e7fa101ba2ea4c631205daa5e0fe357e45
# Parent  73c8987dc9f02d515eb1716f223266404f50e73b
do not use Binding.empty: conceal flag gets lost in Thm.def_binding_optional

diff -r 73c8987dc9f0 -r 2240b0e7fa10 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Mon Nov 02 21:07:10 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Mon Nov 02 22:23:57 2009 +0100
@@ -148,7 +148,8 @@
             val ((f, (_, f_defthm)), lthy') =
               LocalTheory.define Thm.internalK
                 ((Binding.name fname, mixfix),
-                  (apfst Binding.conceal Attrib.empty_binding, Term.subst_bound (fsum, f_def))) lthy
+                  ((Binding.conceal (Binding.name (fname ^ "_def")), []),
+                  Term.subst_bound (fsum, f_def))) lthy
           in
             (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,
                          f=SOME f, f_defthm=SOME f_defthm },