--- a/src/Pure/Thy/export.ML Mon Oct 26 21:35:39 2020 +0100
+++ b/src/Pure/Thy/export.ML Tue Oct 27 22:34:37 2020 +0100
@@ -27,7 +27,7 @@
let
val theory_name = Context.theory_long_name thy;
val (path, pos) = Path.dest_binding binding;
- val markup = Markup.export_path (Path.implode (Path.append (Path.basic theory_name) path));
+ val markup = Markup.export_path (Path.implode (Path.basic theory_name + path));
in Context_Position.report_generic (Context.Theory thy) pos markup end;
type params =
@@ -63,7 +63,7 @@
fun markup thy path =
let
- val thy_path = Path.append (Path.basic (Context.theory_long_name thy)) path;
+ val thy_path = Path.basic (Context.theory_long_name thy) + path;
val name = (Markup.nameN, Path.implode thy_path);
in Active.make_markup Markup.theory_exportsN {implicit = false, properties = [name]} end;