token trans: removed \mbox to achieve proper italic correction;
authorwenzelm
Wed Aug 30 17:54:05 2000 +0200 (2000-08-30)
changeset 974936ddd544a18d
parent 9748 67486cf2f8f6
child 9750 270cd9831e7b
token trans: removed \mbox to achieve proper italic correction;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Aug 30 17:53:23 2000 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Aug 30 17:54:05 2000 +0200
     1.3 @@ -143,8 +143,7 @@
     1.4    in (output_symbols syms, real (Symbol.length syms)) end;
     1.5  
     1.6  val token_translation =
     1.7 -  map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output))
     1.8 -    Syntax.standard_token_classes;
     1.9 +  map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
    1.10  
    1.11  val _ = Symbol.add_mode latexN latex_output;
    1.12  val setup = [Theory.add_tokentrfuns token_translation];