diff -r 0631421c6d6a -r 3e26471d6d01 src/Pure/Thy/export.ML
--- a/src/Pure/Thy/export.ML	Thu Jan 10 19:34:25 2019 +0100
+++ b/src/Pure/Thy/export.ML	Fri Jan 11 10:59:21 2019 +0100
@@ -15,14 +15,10 @@
 
 fun check_name name =
   let
-    fun err () = error ("Bad export name " ^ quote name);
-    fun check_elem elem =
-      if member (op =) ["", ".", ".."] elem then err ()
-      else ignore (Path.basic elem handle ERROR _ => err ());
-
-    val elems = space_explode "/" name;
-    val _ = null elems andalso err ();
-    val _ = List.app check_elem elems;
+    val _ =
+      (case space_explode "/" name of
+        [] => error "Empty export name"
+      | elems => List.app Path.check_elem elems);
   in name end;
 
 fun gen_export compress thy name body =