tuned;
authorwenzelm
Sat, 31 Dec 2022 11:35:28 +0100
changeset 76839 2121fde115b2
parent 76831 72daee8a39ca
child 76840 893eeef9ef08
tuned;
src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Dec 30 21:27:57 2022 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Dec 31 11:35:28 2022 +0100
@@ -93,7 +93,8 @@
 
   def theory_name(s: String): String =
     get_thy_name(s) match {
-      case Some(name) => bootstrap_name(name)
+      case Some(name) =>
+        bootstrap_thys.collectFirst({ case (a, b) if a == name => b }).getOrElse(name)
       case None =>
         Url.get_base_name(s) match {
           case Some(name) =>
@@ -109,9 +110,6 @@
   def is_bootstrap(theory: String): Boolean =
     bootstrap_thys.exists({ case (_, b) => b == theory })
 
-  def bootstrap_name(theory: String): String =
-    bootstrap_thys.collectFirst({ case (a, b) if a == theory => b }).getOrElse(theory)
-
 
   /* parser */