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);