src/Pure/Thy/thy_info.ML
changeset 72235 a5bf0b69c22a
parent 71674 48ff625687f5
child 72311 9a7a14117967
--- a/src/Pure/Thy/thy_info.ML	Tue Sep 01 17:51:20 2020 +0200
+++ b/src/Pure/Thy/thy_info.ML	Tue Sep 01 18:03:17 2020 +0200
@@ -68,10 +68,7 @@
           let
             val latex = Latex.isabelle_body (Context.theory_name thy) body;
             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_binding0 "document.tex") (XML.blob output)
-              else ();
+            val _ = Export.export thy (Path.explode_binding0 "document.tex") (XML.blob output);
             val _ = if #enabled option then Present.theory_output thy output else ();
           in () end
       end));