--- a/src/Pure/Thy/html.ML Thu Jan 11 19:38:37 2001 +0100
+++ b/src/Pure/Thy/html.ML Thu Jan 11 21:51:14 2001 +0100
@@ -130,7 +130,6 @@
("free", color "blue"),
("bound", color "green"),
("var", color "blue"),
- ("xnum", color "yellow"),
("xstr", color "brown")];