diff -r 4b6a5068a128 -r 2a1ca7f6607b src/Pure/PIDE/markup.scala
--- a/src/Pure/PIDE/markup.scala	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/PIDE/markup.scala	Sat Feb 15 18:28:18 2014 +0100
@@ -169,7 +169,9 @@
 
   /* ML syntax */
 
-  val ML_KEYWORD = "ML_keyword"
+  val ML_KEYWORD1 = "ML_keyword1"
+  val ML_KEYWORD2 = "ML_keyword2"
+  val ML_KEYWORD3 = "ML_keyword3"
   val ML_DELIMITER = "ML_delimiter"
   val ML_TVAR = "ML_tvar"
   val ML_NUMERAL = "ML_numeral"