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