author | wenzelm |
Sat, 10 Mar 2012 23:45:47 +0100 | |
changeset 46866 | b190913c3c41 |
parent 46865 | 659dcbafe4bf |
child 46867 | 0883804b67bb |
child 46871 | 9100e6aa9272 |
--- 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 *)