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