--- 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 =