--- a/src/HOL/Tools/Function/function_lib.ML Mon Apr 18 14:26:42 2016 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Mon Apr 18 14:30:24 2016 +0200
@@ -10,7 +10,6 @@
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
@@ -41,8 +40,8 @@
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)
+fun derived_name_suffix binding sffx =
+ Binding.reset_pos (Binding.map_name (suffix sffx) binding)
(* "The variable" ^ plural " is" "s are" vs *)