# HG changeset patch
# User wenzelm
# Date 1636140884 -3600
# Node ID a44d1420705052159921d9fff53d59487d1f8088
# Parent  84e8595a0ec77cbcff61ce804c59c2fec8f8f872
tuned;

diff -r 84e8595a0ec7 -r a44d14207050 src/Pure/Thy/presentation.scala
--- a/src/Pure/Thy/presentation.scala	Fri Nov 05 20:26:07 2021 +0100
+++ b/src/Pure/Thy/presentation.scala	Fri Nov 05 20:34:44 2021 +0100
@@ -430,7 +430,7 @@
           map(link => HTML.text("View ") ::: List(link))).flatten
     }
 
-    val theory_by_name: Map[String, Export_Theory.Theory] =
+    val theory_exports: Map[String, Export_Theory.Theory] =
       (for ((_, entry) <- base.known_theories.iterator) yield {
         val thy_name = entry.name.theory
         val theory =
@@ -461,7 +461,7 @@
           case _ =>
             Some {
               val entities =
-                theory_by_name.get(context.node.theory).flatMap(_.entity_by_range.get(range))
+                theory_exports.get(context.node.theory).flatMap(_.entity_by_range.get(range))
                   .getOrElse(Nil)
               val body1 =
                 if (context.seen_ranges.contains(range)) {
@@ -477,7 +477,7 @@
 
       def entity_ref(thy_name: String, kind: String, name: String): Option[String] =
         for {
-          thy <- theory_by_name.get(thy_name)
+          thy <- theory_exports.get(thy_name)
           entity <- thy.entity_by_kname.get(Export_Theory.export_kind_name(kind, name))
         } yield entity.kname