src/Pure/Thy/present.ML
changeset 72612 878c73cdfa0d
parent 72574 d892f6d66402
child 72613 d01ea9e3bd2d
--- 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";