src/Pure/Thy/export.ML
changeset 70055 36fb663145e5
parent 70051 7a4dc1e60dc8
child 70499 f389019024ce
--- 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);