--- a/src/Pure/Thy/thy_info.ML Sat Mar 30 12:07:31 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML Sat Mar 30 20:54:47 2019 +0100
@@ -66,7 +66,7 @@
val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
val _ =
if Options.bool options "export_document"
- then Export.export thy (Path.explode "document.tex") output else ();
+ then Export.export thy (Path.explode_binding0 "document.tex") output else ();
val _ = if #enabled option then Present.theory_output thy output else ();
in () end
end));