--- a/src/Pure/Thy/thy_info.ML Fri Nov 04 15:34:23 2022 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Nov 04 16:35:39 2022 +0100
@@ -59,14 +59,12 @@
if exists (Toplevel.is_skipped_proof o #state) segments then ()
else
let
- val body = Document_Output.present_thy options (Thy_Header.get_keywords thy) segments;
+ val keywords = Thy_Header.get_keywords thy;
+ val thy_name = Context.theory_name thy;
+ val latex = Document_Output.present_thy options keywords thy_name segments;
in
if Options.string options "document" = "false" then ()
- else
- let
- val thy_name = Context.theory_name thy;
- val latex = Latex.isabelle_body thy_name body;
- in Export.export thy \<^path_binding>\<open>document/latex\<close> latex end
+ else Export.export thy \<^path_binding>\<open>document/latex\<close> latex
end));