# HG changeset patch
# User wenzelm
# Date 965746664 -7200
# Node ID 8d5221bf765b7e54e29c9b4e90768da37f59fdc9
# Parent  c1e730bebcaab75cfb63101471fe6efc130a97e3
token translation: enclose "\\mbox{" "}";

diff -r c1e730bebcaa -r 8d5221bf765b src/Pure/Thy/latex.ML
--- 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];