# HG changeset patch
# User wenzelm
# Date 967650845 -7200
# Node ID 36ddd544a18d0c231c4eb5ec6704a6dfe01fb1d6
# Parent  67486cf2f8f6e16b4bfaaa2edd8251d09865594a
token trans: removed \mbox to achieve proper italic correction;

diff -r 67486cf2f8f6 -r 36ddd544a18d src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Wed Aug 30 17:53:23 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Wed Aug 30 17:54:05 2000 +0200
@@ -143,8 +143,7 @@
   in (output_symbols syms, real (Symbol.length syms)) end;
 
 val token_translation =
-  map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output))
-    Syntax.standard_token_classes;
+  map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
 
 val _ = Symbol.add_mode latexN latex_output;
 val setup = [Theory.add_tokentrfuns token_translation];