--- a/src/Pure/Thy/latex.ML Sun Jun 06 14:20:03 2004 +0200
+++ b/src/Pure/Thy/latex.ML Sun Jun 06 18:35:11 2004 +0200
@@ -17,7 +17,6 @@
val old_symbol_source: string -> Symbol.symbol list -> string
val theory_entry: string -> string
val modes: string list
- val setup: (theory -> theory) list
end;
structure Latex: LATEX =
@@ -149,11 +148,7 @@
fun latex_indent "" = ""
| latex_indent s = enclose "\\isaindent{" "}" s;
-val token_translation =
- map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
-
val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
-val setup = [Theory.add_tokentrfuns token_translation];
end;