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 *)