# HG changeset patch
# User wenzelm
# Date 1513431621 -3600
# Node ID f5d44a01030c7632d85b12bf78094bdb5628f703
# Parent  9e9b78b8e6cac69d41d9e5a7d834febcad24410b
tuned;

diff -r 9e9b78b8e6ca -r f5d44a01030c src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sat Dec 16 14:24:12 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sat Dec 16 14:40:21 2017 +0100
@@ -79,21 +79,21 @@
   val bootstrap_global_theories = (ml_roots ::: bootstrap_thys).map(p => (p._2 -> PURE))
 
   private val Thy_File_Name = new Regex(""".*?([^/\\:]+)\.thy""")
-  private val Import_Name = new Regex(""".*?([^/\\:]+)""")
+  private val File_Name = new Regex(""".*?([^/\\:]+)""")
 
   def is_base_name(s: String): Boolean =
     s != "" && !s.exists("/\\:".contains(_))
 
   def import_name(s: String): String =
     s match {
-      case Import_Name(name) if !name.endsWith(".thy") => name
+      case File_Name(name) if !name.endsWith(".thy") => name
       case _ => error("Malformed theory import: " + quote(s))
     }
 
   def theory_name(s: String): String =
     s match {
       case Thy_File_Name(name) => bootstrap_name(name)
-      case Import_Name(name) =>
+      case File_Name(name) =>
         ml_roots.collectFirst({ case (a, b) if a == name => b }).getOrElse("")
       case _ => ""
     }