# HG changeset patch
# User wenzelm
# Date 1636141326 -3600
# Node ID b2df121ccfc1187e226e24dde06ca484bba98dfb
# Parent  a44d1420705052159921d9fff53d59487d1f8088
more compact persistent data;

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
diff -r a44d14207050 -r b2df121ccfc1 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 20:34:44 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 20:42:06 2021 +0100
@@ -478,7 +478,7 @@
       def entity_ref(thy_name: String, kind: String, name: String): Option[String] =
         for {
           thy <- theory_exports.get(thy_name)
-          entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name))
+          entity <- thy.entity_by_kind_name.get((kind, name))
         } yield entity.kname
 
       def offset_ref(context: Entity_Context, thy_name: String, props: Properties.T): Option[String] =