# HG changeset patch
# User wenzelm
# Date 979246274 -3600
# Node ID 50608ca5785c80f9b549b99d812621300decdcfb
# Parent  87bb4462c43498b1878a5731eef46161ef92e4e0
do not hilite "xnum";

diff -r 87bb4462c434 -r 50608ca5785c src/Pure/Thy/html.ML
--- 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")];