src/Pure/Thy/thy_header.ML
changeset 67164 39f57f0757f1
parent 67139 8fe0aba577af
child 67500 dfde99d59f6e
     1.1 --- a/src/Pure/Thy/thy_header.ML	Fri Dec 08 16:02:44 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_header.ML	Fri Dec 08 17:57:29 2017 +0100
     1.3 @@ -118,7 +118,10 @@
     1.4  fun is_base_name s =
     1.5    s <> "" andalso not (exists_string (member (op =) ["/", "\\", ":"]) s)
     1.6  
     1.7 -val import_name = Path.base_name o Path.explode;
     1.8 +fun import_name s =
     1.9 +  if String.isSuffix ".thy" s then
    1.10 +    error ("Malformed theory import: " ^ quote s)
    1.11 +  else Path.base_name (Path.explode s);
    1.12  
    1.13  
    1.14  (* header args *)