--- a/src/Pure/PIDE/markup.ML Fri Oct 31 18:56:59 2014 +0100
+++ b/src/Pure/PIDE/markup.ML Fri Oct 31 21:10:11 2014 +0100
@@ -162,7 +162,6 @@
val systemN: string
val protocolN: string
val legacyN: string val legacy: T
- val promptN: string val prompt: T
val reportN: string val report: T
val no_reportN: string val no_report: T
val badN: string val bad: T
@@ -547,7 +546,6 @@
val protocolN = "protocol";
val (legacyN, legacy) = markup_elem "legacy";
-val (promptN, prompt) = markup_elem "prompt";
val (reportN, report) = markup_elem "report";
val (no_reportN, no_report) = markup_elem "no_report";