| changeset 71212 | 475510f1a280 |
| parent 70494 | 41108e3e9ca5 |
| child 77841 | de97fcc2c624 |
--- 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 *)