--- a/src/Pure/General/binding.ML Sun Apr 17 22:10:09 2016 +0200
+++ b/src/Pure/General/binding.ML Sun Apr 17 22:38:50 2016 +0200
@@ -25,6 +25,7 @@
val eq_name: binding * binding -> bool
val empty: binding
val is_empty: binding -> bool
+ val conglomerate: binding list -> binding
val qualify: bool -> string -> binding -> binding
val qualify_name: bool -> binding -> string -> binding
val qualified_name: string -> binding
@@ -101,6 +102,9 @@
val empty = name "";
fun is_empty b = name_of b = "";
+fun conglomerate [b] = b
+ | conglomerate bs = name (space_implode "_" (map name_of bs));
+
(* user qualifier *)