--- a/src/HOL/Tools/Function/mutual.ML Sun Sep 06 19:09:20 2015 +0200
+++ b/src/HOL/Tools/Function/mutual.ML Sun Sep 06 21:55:13 2015 +0200
@@ -128,11 +128,13 @@
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), [])
+ else Attrib.empty_binding
val ((f, (_, f_defthm)), lthy') =
Local_Theory.define
((Binding.name fname, mixfix),
- ((Binding.concealed (Binding.name (Thm.def_name fname)), []),
- Term.subst_bound (fsum, f_def))) lthy
+ (def_binding, 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 },