--- a/src/Pure/Thy/export.ML Sun Mar 29 12:30:27 2020 +0200
+++ b/src/Pure/Thy/export.ML Sun Mar 29 13:25:59 2020 +0200
@@ -83,7 +83,10 @@
let
val path = Path.expand (Path.explode ("$ISABELLE_EXPORT_TMP/export" ^ serial_string ()));
val _ = YXML.write_body path body;
- in Protocol_Message.inline (#2 function) (tl args @ [(Markup.fileN, Path.implode path)]) end
+ in
+ Protocol_Message.inline_properties (#2 function)
+ (tl args @ [(Markup.fileN, Path.implode path)])
+ end
else raise Output.Protocol_Message props
| [] => raise Output.Protocol_Message props);