diff -r 04d39959d1e6 -r b5fb99b985b4 src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Tue May 25 23:18:29 2021 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue May 25 23:37:32 2021 +0200
@@ -30,14 +30,6 @@
 
 (** theory presentation **)
 
-(* artefact names *)
-
-fun document_name ext thy =
-  Path.explode_binding0 ("document/" ^ Context.theory_name thy ^ "." ^ ext);
-
-val document_tex_name = document_name "tex";
-
-
 (* hook for consolidated theory *)
 
 type presentation_context =
@@ -77,9 +69,8 @@
         else
           let
             val thy_name = Context.theory_name thy;
-            val document_tex_name = document_tex_name thy;
             val latex = Latex.isabelle_body thy_name body;
-          in Export.export thy document_tex_name latex end
+          in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end
       end));