--- a/src/Pure/Thy/thy_header.ML Fri Dec 08 16:02:44 2017 +0100
+++ b/src/Pure/Thy/thy_header.ML Fri Dec 08 17:57:29 2017 +0100
@@ -118,7 +118,10 @@
fun is_base_name s =
s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
-val import_name = Path.base_name o Path.explode;
+fun import_name s =
+ if String.isSuffix ".thy" s then
+ error ("Malformed theory import: " ^ quote s)
+ else Path.base_name (Path.explode s);
(* header args *)
--- a/src/Pure/Thy/thy_header.scala Fri Dec 08 16:02:44 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala Fri Dec 08 17:57:29 2017 +0100
@@ -85,7 +85,10 @@
s != "" && !s.exists("/\\:".contains(_))
def import_name(s: String): String =
- s match { case Import_Name(name) => name case _ => error("Malformed import: " + quote(s)) }
+ s match {
+ case Import_Name(name) if !name.endsWith(".thy") => name
+ case _ => error("Malformed theory import: " + quote(s))
+ }
def theory_name(s: String): String =
s match {