more robust;
authorwenzelm
Mon, 02 Dec 2019 13:33:45 +0100
changeset 71212 475510f1a280
parent 71211 7d522732b7f2
child 71213 39ccdbbed539
more robust;
src/Pure/General/binding.ML
--- a/src/Pure/General/binding.ML	Mon Dec 02 13:03:09 2019 +0100
+++ b/src/Pure/General/binding.ML	Mon Dec 02 13:33:45 2019 +0100
@@ -122,7 +122,7 @@
 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));
+  | conglomerate bs = name (space_implode "_" (map name_of (filter_out is_empty bs)));
 
 
 (* user qualifier *)