diff -r d983509dbf31 -r b275f26a638b src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 21:59:35 2009 +0100
+++ b/src/HOL/Tools/Function/mutual.ML	Thu Nov 12 22:02:11 2009 +0100
@@ -146,7 +146,7 @@
       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
+              LocalTheory.define ""
                 ((Binding.name fname, mixfix),
                   ((Binding.conceal (Binding.name (fname ^ "_def")), []),
                   Term.subst_bound (fsum, f_def))) lthy