diff -r e344dc82f6c2 -r 4eaf35781b23 src/Pure/General/binding.ML
--- 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));