src/Pure/General/markup.ML
changeset 34214 99eefb83a35d
parent 34212 8c3e1f73953d
child 34250 5ccdc8bf3849
     1.1 --- a/src/Pure/General/markup.ML	Wed Dec 30 22:29:37 2009 +0100
     1.2 +++ b/src/Pure/General/markup.ML	Wed Dec 30 22:56:46 2009 +0100
     1.3 @@ -107,7 +107,6 @@
     1.4    val disposedN: string val disposed: T
     1.5    val editN: string val edit: string -> string -> T
     1.6    val pidN: string
     1.7 -  val sessionN: string
     1.8    val promptN: string val prompt: T
     1.9    val readyN: string val ready: T
    1.10    val no_output: output * output
    1.11 @@ -313,7 +312,6 @@
    1.12  (* messages *)
    1.13  
    1.14  val pidN = "pid";
    1.15 -val sessionN = "session";
    1.16  
    1.17  val (promptN, prompt) = markup_elem "prompt";
    1.18  val (readyN, ready) = markup_elem "ready";