# HG changeset patch
# User wenzelm
# Date 1575290025 -3600
# Node ID 475510f1a280b82016d8eae79c94deaebee7e833
# Parent  7d522732b7f2c98a1434588f8bb124cffb154d9f
more robust;

diff -r 7d522732b7f2 -r 475510f1a280 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 *)