diff -r 17d431c92575 -r d138e7482a1b src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Wed Jun 22 20:25:35 2011 +0200
+++ b/src/Pure/Thy/html.scala	Wed Jun 22 20:38:03 2011 +0200
@@ -82,13 +82,13 @@
             val s1 = syms.next
             def s2() = if (syms.hasNext) syms.next else ""
             if (s1 == "\n") add(XML.elem(BR))
-            else if (s1 == "\\<^bsub>") t ++= s1  // FIXME
-            else if (s1 == "\\<^esub>") t ++= s1  // FIXME
-            else if (s1 == "\\<^bsup>") t ++= s1  // FIXME
-            else if (s1 == "\\<^esup>") t ++= s1  // FIXME
+            else if (s1 == symbols.bsub_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.esub_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.bsup_decoded) t ++= s1  // FIXME
+            else if (s1 == symbols.esup_decoded) t ++= s1  // FIXME
             else if (symbols.is_subscript_decoded(s1)) { add(hidden(s1)); add(sub(s2())) }
             else if (symbols.is_superscript_decoded(s1)) { add(hidden(s1)); add(sup(s2())) }
-            else if (symbols.is_bold_decoded(s1)) { add(hidden(s1)); add(bold(s2())) }
+            else if (s1 == symbols.bold_decoded) { add(hidden(s1)); add(bold(s2())) }
             else if (symbols.fonts.isDefinedAt(s1)) { add(user_font(symbols.fonts(s1), s1)) }
             else t ++= s1
           }