# HG changeset patch
# User wenzelm
# Date 1256743668 -3600
# Node ID 6b086276bbf7651a9707352fa09dd329c4a50090
# Parent  ba9f52f56356b90441e771793bb2b64f67079946
simplified default binding;
conceal internal bindings;

diff -r ba9f52f56356 -r 6b086276bbf7 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 16:25:27 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Wed Oct 28 16:27:48 2009 +0100
@@ -146,9 +146,9 @@
       fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
           let
             val ((f, (_, f_defthm)), lthy') =
-              LocalTheory.define Thm.internalK ((Binding.name fname, mixfix),
-                                            ((Binding.name (fname ^ "_def"), []), Term.subst_bound (fsum, f_def)))
-                              lthy
+              LocalTheory.define Thm.internalK
+                ((Binding.name fname, mixfix),
+                  (apfst Binding.conceal Attrib.empty_binding, 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 },