diff -r 72daee8a39ca -r 2121fde115b2 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 */