src/Pure/Thy/thy_header.scala

--- a/src/Pure/Thy/thy_header.scala	Thu Dec 28 14:20:48 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Thu Dec 28 21:45:28 2017 +0100
@@ -85,6 +85,12 @@
   def is_base_name(s: String): Boolean =
     s != "" && !s.exists("/\\:".contains(_))
 
+  def file_name(s: String): Option[String] =
+    s match {
+      case File_Name(s) => Some(s)
+      case _ => None
+    }
+
   def import_name(s: String): String =
     s match {
       case File_Name(name) if !name.endsWith(".thy") => name