--- a/src/HOL/Tools/Function/function.ML Sun Apr 17 22:10:09 2016 +0200
+++ b/src/HOL/Tools/Function/function.ML Sun Apr 17 22:38:50 2016 +0200
@@ -78,11 +78,7 @@
val (eqs, post, sort_cont, cnames) = get_preproc lthy config ctxt' fixes spec
val fnames = map (fst o fst) fixes0
- val f_base_names = map (fst o fst) fixes
- val defname =
- (case fixes0 of
- [((b, _), _)] => b
- | _ => Binding.name (space_implode "_" f_base_names))
+ val defname = Binding.conglomerate fnames;
val FunctionConfig {partials, default, ...} = config
val _ =