src/Pure/Thy/html.ML
changeset 46866 b190913c3c41
parent 45666 d83797ef0d2d
child 48670 206144b13849
--- a/src/Pure/Thy/html.ML	Sat Mar 10 23:28:42 2012 +0100
+++ b/src/Pure/Thy/html.ML	Sat Mar 10 23:45:47 2012 +0100
@@ -48,12 +48,7 @@
 
 fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
 
-fun span_class (name, props) =
-  (case Isabelle_Markup.get_entity_kind (name, props) of
-    SOME kind => Isabelle_Markup.entityN ^ "_" ^ name
-  | NONE => name);
-
-val _ = Markup.add_mode htmlN (span o span_class);
+val _ = Markup.add_mode htmlN (span o fst);
 
 
 (* symbol output *)