diff -r 5df087c6ce94 -r 8e51fc35d59f src/Pure/General/markup.scala --- a/src/Pure/General/markup.scala Tue May 25 22:21:31 2010 +0200 +++ b/src/Pure/General/markup.scala Tue May 25 23:03:13 2010 +0200 @@ -193,7 +193,6 @@ val INIT = "init" val STATUS = "status" val WRITELN = "writeln" - val PRIORITY = "priority" val TRACING = "tracing" val WARNING = "warning" val ERROR = "error"