token translation: enclose "\\mbox{" "}";

--- a/src/Pure/Thy/latex.ML	Tue Aug 08 16:39:34 2000 +0200
+++ b/src/Pure/Thy/latex.ML	Tue Aug 08 16:57:44 2000 +0200
@@ -121,7 +121,9 @@
   let val syms = Symbol.explode str
   in (output_symbols syms, real (Symbol.length syms)) end;
 
-val token_translation = map (fn s => (latexN, s, latex_output)) Syntax.standard_token_classes;
+val token_translation =
+  map (fn s => (latexN, s, apfst (enclose "\\mbox{" "}") o latex_output))
+    Syntax.standard_token_classes;
 
 val _ = Symbol.add_mode latexN latex_output;
 val setup = [Theory.add_tokentrfuns token_translation];