src/HOL/Tools/Function/mutual.ML

 fun define_projections fixes mutual fsum lthy =
   let
     fun def ((MutualPart {i=i, i'=i', fvar=(fname, fT), cargTs, f_def, ...}), (_, mixfix)) lthy =
       let
         val def_binding =
-          if Config.get lthy function_defs then (Binding.name (Thm.def_name fname), [])
+          if Config.get lthy function_internals then (Binding.name (Thm.def_name fname), [])
           else Attrib.empty_binding
         val ((f, (_, f_defthm)), lthy') =
           Local_Theory.define
             ((Binding.name fname, mixfix),
               (def_binding, Term.subst_bound (fsum, f_def))) lthy