diff -r 890b68e1e8b6 -r f9d1442c70f3 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Mon Mar 30 22:34:59 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Tue Mar 31 00:11:54 2015 +0200
@@ -131,7 +131,7 @@
         val ((f, (_, f_defthm)), lthy') =
           Local_Theory.define
             ((Binding.name fname, mixfix),
-              ((Binding.conceal (Binding.name (Thm.def_name fname)), []),
+              ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
               Term.subst_bound (fsum, f_def))) lthy
       in
         (MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs=cargTs, f_def=f_def,