diff -r bf5fcc65586b -r f507e6fe1d77 src/HOL/Tools/Function/mutual.ML
--- a/src/HOL/Tools/Function/mutual.ML	Sun Apr 17 20:11:02 2016 +0200
+++ b/src/HOL/Tools/Function/mutual.ML	Sun Apr 17 20:54:17 2016 +0200
@@ -7,7 +7,7 @@
 signature FUNCTION_MUTUAL =
 sig
   val prepare_function_mutual : Function_Common.function_config
-    -> string (* defname *)
+    -> binding (* defname *)
     -> ((string * typ) * mixfix) list
     -> term list
     -> local_theory
@@ -90,7 +90,8 @@
 
     val fsum_type = ST --> RST
 
-    val ([fsum_var_name], _) = Variable.add_fixes [ defname ^ "_sum" ] ctxt
+    val ([fsum_var_name], _) =
+      Variable.add_fixes_binding [Binding.map_name (suffix "_sum") defname] ctxt
     val fsum_var = (fsum_var_name, fsum_type)
 
     fun define (fvar as (n, _)) caTs resultT i =