type Path.binding may be empty: check later via proper_binding;
clarified 'export_prefix' default;

--- a/src/Pure/General/path.ML	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/General/path.ML	Thu Apr 04 20:45:55 2019 +0200
@@ -45,6 +45,7 @@
   val dest_binding: binding -> T * Position.T
   val path_of_binding: binding -> T
   val pos_of_binding: binding -> Position.T
+  val proper_binding: binding -> unit
   val implode_binding: binding -> string
   val explode_binding: string * Position.T -> binding
   val explode_binding0: string -> binding
@@ -262,7 +263,7 @@
 datatype binding = Binding of T * Position.T;
 
 fun binding (path, pos) =
-  if not (is_current path) andalso all_basic path then Binding (path, pos)
+  if all_basic path then Binding (path, pos)
   else error ("Bad path binding: " ^ print path ^ Position.here pos);
 
 fun binding0 path = binding (path, Position.none);
@@ -273,6 +274,11 @@
 val path_of_binding = dest_binding #> #1;
 val pos_of_binding = dest_binding #> #2;
 
+fun proper_binding binding =
+  if is_current (path_of_binding binding)
+  then error ("Empty path" ^ Position.here (pos_of_binding binding))
+  else ();
+
 val implode_binding = path_of_binding #> implode_path;
 
 val explode_binding = binding o explode_pos;

--- a/src/Pure/Pure.thy	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/Pure.thy	Thu Apr 04 20:45:55 2019 +0200
@@ -157,7 +157,7 @@
       (Parse.and_list files_in --
         Scan.optional (\<^keyword>\<open>external_files\<close> |-- Parse.!!! (Parse.and_list1 external_files)) [] --
         Scan.optional (\<^keyword>\<open>export_files\<close> |-- Parse.!!! (Parse.and_list1 export_files)) [] --
-        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("compiled", Position.none) --
+        Scan.optional (\<^keyword>\<open>export_prefix\<close> |-- Parse.path_binding) ("", Position.none) --
         (Parse.where_ |-- Parse.!!! Parse.ML_source)
         >> (fn ((((args, external), export), export_prefix), source) =>
           Toplevel.keep (fn st =>

--- a/src/Pure/Thy/export.ML	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/Thy/export.ML	Thu Apr 04 20:45:55 2019 +0200
@@ -37,7 +37,7 @@
    {id = Position.get_id (Position.thread_data ()),
     serial = serial (),
     theory_name = Context.theory_long_name thy,
-    name = Path.implode_binding binding,
+    name = Path.implode_binding (tap Path.proper_binding binding),
     executable = executable,
     compress = compress} blob);
 

--- a/src/Pure/Tools/generated_files.ML	Thu Apr 04 16:47:09 2019 +0200
+++ b/src/Pure/Tools/generated_files.ML	Thu Apr 04 20:45:55 2019 +0200
@@ -74,7 +74,10 @@
 );
 
 fun add_files (binding, content) =
-  let val (path, pos) = Path.dest_binding binding in
+  let
+    val _ = Path.proper_binding binding;
+    val (path, pos) = Path.dest_binding binding;
+  in
     (Data.map o @{apply 3(1)}) (fn files =>
       (case AList.lookup (op =) files path of
         SOME (pos', _) =>