avoid interference of markup for literal tokens, which may contain slightly odd \<^bsub> \<^esub> counted as pseudo-markup (especially relevant for HTML output, e.g. of thm power3_eq_cube);

--- a/src/Pure/General/symbol.ML	Wed May 02 16:04:07 2012 +0200
+++ b/src/Pure/General/symbol.ML	Wed May 02 16:56:25 2012 +0200
@@ -48,6 +48,7 @@
   val is_digit: symbol -> bool
   val is_quasi: symbol -> bool
   val is_blank: symbol -> bool
+  val is_block_ctrl: symbol -> bool
   val is_quasi_letter: symbol -> bool
   val is_letdig: symbol -> bool
   val is_ident: symbol list -> bool
@@ -390,6 +391,8 @@
 fun is_quasi s = kind s = Quasi;
 fun is_blank s = kind s = Blank;
 
+val is_block_ctrl = member (op =) ["\\<^bsub>", "\\<^esub>", "\\<^bsup>", "\\<^esup>"];
+
 fun is_quasi_letter s = let val k = kind s in k = Letter orelse k = Quasi end;
 fun is_letdig s = let val k = kind s in k = Letter orelse k = Digit orelse k = Quasi end;
 

--- a/src/Pure/Syntax/printer.ML	Wed May 02 16:04:07 2012 +0200
+++ b/src/Pure/Syntax/printer.ML	Wed May 02 16:56:25 2012 +0200
@@ -191,8 +191,13 @@
                 tabs trf token_trans markup_extern t @ Ts, args')
           end
       | synT m (String s :: symbs, args) =
-          let val (Ts, args') = synT m (symbs, args);
-          in (Pretty.marks_str (m, s) :: Ts, args') end
+          let
+            val (Ts, args') = synT m (symbs, args);
+            val T =
+              if exists Symbol.is_block_ctrl (Symbol.explode s)
+              then Pretty.str s
+              else Pretty.marks_str (m, s);
+          in (T :: Ts, args') end
       | synT m (Space s :: symbs, args) =
           let val (Ts, args') = synT m (symbs, args);
           in (Pretty.str s :: Ts, args') end