1.1 --- a/src/Pure/Thy/latex.ML	Sun Jan 21 19:54:52 2001 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Sun Jan 21 19:55:25 2001 +0100
     1.3 @@ -144,10 +144,13 @@
     1.4    let val syms = Symbol.explode str
     1.5    in (output_symbols syms, real (Symbol.length syms)) end;
     1.6  
     1.7 +fun latex_indent "" = ""
     1.8 +  | latex_indent s = enclose "\\isaindent{" "}" s;
     1.9 +
    1.10  val token_translation =
    1.11    map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
    1.12  
    1.13 -val _ = Symbol.add_mode latexN latex_output;
    1.14 +val _ = Symbol.add_mode latexN (latex_output, latex_indent o #1);
    1.15  val setup = [Theory.add_tokentrfuns token_translation];
    1.16  
    1.17