author | wenzelm |
Mon, 02 Dec 2019 13:33:45 +0100 | |
changeset 71212 | 475510f1a280 |
parent 71211 | 7d522732b7f2 |
child 71213 | 39ccdbbed539 |
--- 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 *)