--- a/src/HOL/Tools/Function/mutual.ML Thu Jan 07 15:50:09 2016 +0100
+++ b/src/HOL/Tools/Function/mutual.ML Thu Jan 07 15:53:39 2016 +0100
@@ -129,7 +129,7 @@
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