src/Pure/Thy/thy_header.scala
changeset 76890 d924a69e7d2b
parent 76839 2121fde115b2
child 77011 3e48f8c6afc9
--- 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 =