1.1 --- a/src/Pure/Thy/latex.ML	Sun Jun 06 14:20:03 2004 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Jun 06 18:35:11 2004 +0200
     1.3 @@ -17,7 +17,6 @@
     1.4    val old_symbol_source: string -> Symbol.symbol list -> string
     1.5    val theory_entry: string -> string
     1.6    val modes: string list
     1.7 -  val setup: (theory -> theory) list
     1.8  end;
     1.9  
    1.10  structure Latex: LATEX =
    1.11 @@ -149,11 +148,7 @@
    1.12  fun latex_indent "" = ""
    1.13    | latex_indent s = enclose "\\isaindent{" "}" s;
    1.14  
    1.15 -val token_translation =
    1.16 -  map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
    1.17 -
    1.18  val _ = Output.add_mode latexN (latex_output, latex_indent o #1, Symbol.default_raw);
    1.19 -val setup = [Theory.add_tokentrfuns token_translation];
    1.20  
    1.21  
    1.22  end;

     2.1 --- a/src/Pure/pure.ML	Sun Jun 06 14:20:03 2004 +0200
     2.2 +++ b/src/Pure/pure.ML	Sun Jun 06 18:35:11 2004 +0200
     2.3 @@ -19,7 +19,6 @@
     2.4      Calculation.setup @
     2.5      SkipProof.setup @
     2.6      AxClass.setup @
     2.7 -    Latex.setup @
     2.8      Present.setup @
     2.9      ProofGeneral.setup @
    2.10      Codegen.setup @