diff -r 98993083e4ac -r d924a69e7d2b src/Pure/Thy/thy_header.scala --- a/src/Pure/Thy/thy_header.scala Tue Jan 03 20:46:56 2023 +0100 +++ b/src/Pure/Thy/thy_header.scala Tue Jan 03 21:18:15 2023 +0100 @@ -84,11 +84,9 @@ def get_thy_name(s: String): Option[String] = Url.get_base_name(s, suffix = ".thy") - def list_thy_names(dir: Path): List[String] = { - val files = - try { File.read_dir(dir) } - catch { case ERROR(_) => Nil } - files.flatMap(get_thy_name) + def list_thys(dir: Path): List[String] = { + val entries = try { File.read_dir(dir) } catch { case ERROR(_) => Nil } + entries.flatMap(get_thy_name) } def theory_name(s: String): String =