--- 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")];
changeset 10873	50608ca5785c
parent 10837	7d640de604e4
child 10954	a555bfb66c2d