# HG changeset patch
# User wenzelm
# Date 1512752249 -3600
# Node ID 39f57f0757f185b707181b175e8ba3d9da9e59aa
# Parent  257bcd20eeecdb154d55fb14b06aa15810ba4984
clarified error;

diff -r 257bcd20eeec -r 39f57f0757f1 src/Pure/Thy/thy_header.ML
--- 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 *)
diff -r 257bcd20eeec -r 39f57f0757f1 src/Pure/Thy/thy_header.scala
--- 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 {