src/HOL/Tools/Function/mutual.ML

 *)
 
 signature FUNCTION_MUTUAL =
 sig
   val prepare_function_mutual : Function_Common.function_config
-    -> string (* defname *)
+    -> binding (* defname *)
     -> ((string * typ) * mixfix) list
     -> term list
     -> local_theory
     -> ((thm (* goalstate *)
         * (Proof.context -> thm -> Function_Common.function_result) (* proof continuation *)

     val RST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) dresultTs
     val ST = Balanced_Tree.make (uncurry Sum_Tree.mk_sumT) argTs
 
     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 =
       let
         val vars = map_index (fn (j,T) => Free ("x" ^ string_of_int j, T)) caTs (* FIXME: Bind xs properly *)