# HG changeset patch
# User wenzelm
# Date 1605371377 -3600
# Node ID 878c73cdfa0d968fecf331511d949a5e041fcc04
# Parent  b6bce47d0b48fcd5751afa100bea12997fe542ac
tuned signature;

diff -r b6bce47d0b48 -r 878c73cdfa0d src/Pure/Thy/present.ML
--- a/src/Pure/Thy/present.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Thy/present.ML	Sat Nov 14 17:29:37 2020 +0100
@@ -6,7 +6,6 @@
 
 signature PRESENT =
 sig
-  val tex_path: string -> Path.T
   val get_bibtex_entries: theory -> string list
   val theory_qualifier: theory -> string
   val init: HTML.symbols -> bool -> Path.T -> string list -> string * string -> bool -> unit
@@ -20,8 +19,6 @@
 
 (** paths **)
 
-val tex_ext = Path.ext "tex";
-val tex_path = tex_ext o Path.basic;
 val html_ext = Path.ext "html";
 val html_path = html_ext o Path.basic;
 val index_path = Path.basic "index.html";
diff -r b6bce47d0b48 -r 878c73cdfa0d src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Sat Nov 14 16:53:18 2020 +0100
+++ b/src/Pure/Thy/thy_info.ML	Sat Nov 14 17:29:37 2020 +0100
@@ -66,11 +66,10 @@
         else
           let
             val thy_name = Context.theory_name thy;
-            val document_path = Path.basic "document" + Present.tex_path thy_name;
-
+            val document_tex_name = Path.explode_binding0 ("document/" ^ thy_name ^ ".tex");
             val latex = Latex.isabelle_body thy_name body;
             val output = [Latex.output_text latex, Latex.output_positions file_pos latex];
-          in Export.export thy (Path.binding0 document_path) (XML.blob output) end
+          in Export.export thy document_tex_name (XML.blob output) end
       end));