less redundant;

--- a/src/Pure/Thy/html.ML	Sat Dec 30 21:46:19 2017 +0100
+++ b/src/Pure/Thy/html.ML	Sat Dec 30 22:37:07 2017 +0100
@@ -24,7 +24,9 @@
 
 (* common markup *)
 
-fun span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+fun span "" = ("<span>", "</span>")
+  | span class = ("<span class=" ^ quote (XML.text class) ^ ">", "</span>");
+
 val enclose_span = uncurry enclose o span;
 
 val hidden = enclose_span Markup.hiddenN;