clarified Path.check_elem;

--- a/src/Pure/General/path.ML	Thu Jan 10 19:34:25 2019 +0100
+++ b/src/Pure/General/path.ML	Fri Jan 11 10:59:21 2019 +0100
@@ -7,6 +7,7 @@
 
 signature PATH =
 sig
+  val check_elem: string -> unit
   eqtype T
   val is_current: T -> bool
   val current: T
@@ -56,7 +57,9 @@
 val illegal_elem = ["", "~", "~~", ".", ".."];
 val illegal_char = ["/", "\\", "$", ":", "\"", "'", "<", ">", "|", "?", "*"];
 
-val check_elem = tap (fn s =>
+in
+
+fun check_elem s =
   if member (op =) illegal_elem s then err_elem "Illegal" s
   else
     (s, ()) |-> fold_string (fn c => fn () =>
@@ -64,13 +67,11 @@
         err_elem ("Illegal control character " ^ string_of_int (ord c) ^ " in") s
       else if member (op =) illegal_char c then
         err_elem ("Illegal character " ^ quote c ^ " in") s
-      else ()));
-
-in
+      else ());
 
-val root_elem = Root o check_elem;
-val basic_elem = Basic o check_elem;
-val variable_elem = Variable o check_elem;
+val root_elem = Root o tap check_elem;
+val basic_elem = Basic o tap check_elem;
+val variable_elem = Variable o tap check_elem;
 
 end;
 

--- 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 =