src/Pure/Thy/thy_header.scala
changeset 67164 39f57f0757f1
parent 67013 335a7dce7cb3
child 67212 f5d44a01030c
     1.1 --- a/src/Pure/Thy/thy_header.scala	Fri Dec 08 16:02:44 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Fri Dec 08 17:57:29 2017 +0100
     1.3 @@ -85,7 +85,10 @@
     1.4      s != "" && !s.exists("/\\:".contains(_))
     1.5  
     1.6    def import_name(s: String): String =
     1.7 -    s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
     1.8 +    s match {
     1.9 +      case Import_Name(name) if !name.endsWith(".thy") => name
    1.10 +      case _ => error("Malformed theory import: " + quote(s))
    1.11 +    }
    1.12  
    1.13    def theory_name(s: String): String =
    1.14      s match {