# HG changeset patch
# User wenzelm
# Date 1514669827 -3600
# Node ID 897344e33c26cb8614b442dd0ca4832f4e692d6f
# Parent  ecb74607063f4928b1635fa3b04f5002b0e2dbf4
less redundant;

diff -r ecb74607063f -r 897344e33c26 src/Pure/Thy/html.ML
--- 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;