diff -r f507e6fe1d77 -r d743bb1b6c23 src/HOL/Tools/Function/function_lib.ML
--- a/src/HOL/Tools/Function/function_lib.ML	Sun Apr 17 20:54:17 2016 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML	Sun Apr 17 22:10:09 2016 +0200
@@ -9,6 +9,10 @@
 sig
   val function_internals: bool Config.T
 
+  val derived_name: binding -> string -> binding
+  val name_suffix: binding -> string -> binding
+  val derived_name_suffix: binding -> string -> binding
+
   val plural: string -> string -> 'a list -> string
 
   val dest_all_all: term -> term list * term
@@ -34,6 +38,12 @@
 
 val function_internals = Attrib.setup_config_bool @{binding function_internals} (K false)
 
+fun derived_name binding name =
+  Binding.reset_pos (Binding.qualify_name true binding name)
+
+fun name_suffix binding sffx = Binding.map_name (suffix sffx) binding
+fun derived_name_suffix binding sffx = Binding.reset_pos (name_suffix binding sffx)
+
 
 (* "The variable" ^ plural " is" "s are" vs *)
 fun plural sg pl [x] = sg