token trans: removed \mbox to achieve proper italic correction;

--- 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];