--- 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 */