# HG changeset patch
# User wenzelm
# Date 1086539711 -7200
# Node ID 8989eedf72a1919b115151ad9305e3cb7cda6f24
# Parent  b884a7ba723847754435736b8d4f561175cd3d19
no token translation / setup for Latex;

diff -r b884a7ba7238 -r 8989eedf72a1 src/Pure/Thy/latex.ML
--- 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;
diff -r b884a7ba7238 -r 8989eedf72a1 src/Pure/pure.ML
--- a/src/Pure/pure.ML	Sun Jun 06 14:20:03 2004 +0200
+++ b/src/Pure/pure.ML	Sun Jun 06 18:35:11 2004 +0200
@@ -19,7 +19,6 @@
     Calculation.setup @
     SkipProof.setup @
     AxClass.setup @
-    Latex.setup @
     Present.setup @
     ProofGeneral.setup @
     Codegen.setup @