src/Pure/ML/ml_lex.ML

--- a/src/Pure/ML/ml_lex.ML	Tue Aug 17 23:23:29 2010 +0200
+++ b/src/Pure/ML/ml_lex.ML	Wed Aug 18 11:02:47 2010 +0200
@@ -100,10 +100,10 @@
   | Real      => Markup.ML_numeral
   | Char      => Markup.ML_char
   | String    => Markup.ML_string
-  | Space     => Markup.none
+  | Space     => Markup.empty
   | Comment   => Markup.ML_comment
   | Error _   => Markup.ML_malformed
-  | EOF       => Markup.none;
+  | EOF       => Markup.empty;
 
 fun token_markup kind x =
   if kind = Keyword andalso exists_string (not o Symbol.is_ascii_letter) x