diff -r 4b6a5068a128 -r 2a1ca7f6607b src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Sat Feb 15 17:10:57 2014 +0100
+++ b/src/Pure/PIDE/markup.ML	Sat Feb 15 18:28:18 2014 +0100
@@ -68,7 +68,9 @@
   val propN: string val prop: T
   val sortingN: string val sorting: T
   val typingN: string val typing: T
-  val ML_keywordN: string val ML_keyword: T
+  val ML_keyword1N: string val ML_keyword1: T
+  val ML_keyword2N: string val ML_keyword2: T
+  val ML_keyword3N: string val ML_keyword3: T
   val ML_delimiterN: string val ML_delimiter: T
   val ML_tvarN: string val ML_tvar: T
   val ML_numeralN: string val ML_numeral: T
@@ -325,7 +327,9 @@
 
 (* ML syntax *)
 
-val (ML_keywordN, ML_keyword) = markup_elem "ML_keyword";
+val (ML_keyword1N, ML_keyword1) = markup_elem "ML_keyword1";
+val (ML_keyword2N, ML_keyword2) = markup_elem "ML_keyword2";
+val (ML_keyword3N, ML_keyword3) = markup_elem "ML_keyword3";
 val (ML_delimiterN, ML_delimiter) = markup_elem "ML_delimiter";
 val (ML_tvarN, ML_tvar) = markup_elem "ML_tvar";
 val (ML_numeralN, ML_numeral) = markup_elem "ML_numeral";