--- a/src/Pure/General/binding.ML Wed Jun 22 16:04:03 2016 +0200
+++ b/src/Pure/General/binding.ML Thu Jun 23 11:01:14 2016 +0200
@@ -25,6 +25,8 @@
val eq_name: binding * binding -> bool
val empty: binding
val is_empty: binding -> bool
+ val empty_atts: binding * 'a list
+ val is_empty_atts: binding * 'a list -> bool
val conglomerate: binding list -> binding
val qualify: bool -> string -> binding -> binding
val qualify_name: bool -> binding -> string -> binding
@@ -102,6 +104,9 @@
val empty = name "";
fun is_empty b = name_of b = "";
+val empty_atts = (empty, []);
+fun is_empty_atts (b, atts) = is_empty b andalso null atts;
+
fun conglomerate [b] = b
| conglomerate bs = name (space_implode "_" (map name_of bs));