diff -r 9e86c1ca6e51 -r 99eefb83a35d src/Pure/General/markup.ML
--- a/src/Pure/General/markup.ML	Wed Dec 30 22:29:37 2009 +0100
+++ b/src/Pure/General/markup.ML	Wed Dec 30 22:56:46 2009 +0100
@@ -107,7 +107,6 @@
   val disposedN: string val disposed: T
   val editN: string val edit: string -> string -> T
   val pidN: string
-  val sessionN: string
   val promptN: string val prompt: T
   val readyN: string val ready: T
   val no_output: output * output
@@ -313,7 +312,6 @@
 (* messages *)
 
 val pidN = "pid";
-val sessionN = "session";
 
 val (promptN, prompt) = markup_elem "prompt";
 val (readyN, ready) = markup_elem "ready";