diff -r a44d14207050 -r b2df121ccfc1 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Fri Nov 05 20:34:44 2021 +0100 +++ b/src/Pure/Thy/export_theory.scala Fri Nov 05 20:42:06 2021 +0100 @@ -97,8 +97,8 @@ lazy val entity_by_range: Map[Symbol.Range, List[Entity[No_Content]]] = entity_iterator.toList.groupBy(_.range) - lazy val entity_by_kname: Map[String, Entity[No_Content]] = - entity_iterator.map(entity => (entity.kname, entity)).toMap + lazy val entity_by_kind_name: Map[(String, String), Entity[No_Content]] = + entity_iterator.map(entity => ((entity.kind, entity.name), entity)).toMap lazy val entity_kinds: Set[String] = entity_iterator.map(_.kind).toSet