diff -r beb9a8695263 -r 8cdddd689ea9 src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Sun May 30 13:47:12 2010 +0200
+++ b/src/Pure/General/markup.ML	Sun May 30 14:14:30 2010 +0200
@@ -83,6 +83,7 @@
   val keyword_declN: string val keyword_decl: string -> T
   val command_declN: string val command_decl: string -> string -> T
   val keywordN: string val keyword: string -> T
+  val operatorN: string val operator: T
   val commandN: string val command: string -> T
   val identN: string val ident: T
   val stringN: string val string: T
@@ -271,6 +272,7 @@
 fun command_decl name kind : T = (command_declN, [(nameN, name), (kindN, kind)]);
 
 val (keywordN, keyword) = markup_string "keyword" nameN;
+val (operatorN, operator) = markup_elem "operator";
 val (commandN, command) = markup_string "command" nameN;
 val (identN, ident) = markup_elem "ident";
 val (stringN, string) = markup_elem "string";