--- 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";