diff -r 129db1416717 -r d83797ef0d2d src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Mon Nov 28 20:39:08 2011 +0100
+++ b/src/Pure/Thy/html.scala	Mon Nov 28 22:05:32 2011 +0100
@@ -49,7 +49,7 @@
     XML.Elem(Markup(SPAN, List((STYLE, "font-family: " + font))), List(XML.Text(txt)))
 
   def hidden(txt: String): XML.Elem =
-    span(Markup.HIDDEN, List(XML.Text(txt)))
+    span(Isabelle_Markup.HIDDEN, List(XML.Text(txt)))
 
   def sub(txt: String): XML.Elem = XML.elem("sub", List(XML.Text(txt)))
   def sup(txt: String): XML.Elem = XML.elem("sup", List(XML.Text(txt)))
@@ -61,7 +61,7 @@
       tree match {
         case XML.Elem(m @ Markup(name, props), ts) =>
           val span_class =
-            m match { case Markup.Entity(kind, _) => name + "_" + kind case _ => name }
+            m match { case Isabelle_Markup.Entity(kind, _) => name + "_" + kind case _ => name }
           val html_span = span(span_class, ts.flatMap(html_spans))
           if (original_data) List(XML.Elem(Markup.Data, List(tree, html_span)))
           else List(html_span)