--- 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 },