diff -r 6dd13e111d30 -r 22c87ff1b8a9 src/Pure/General/yxml.ML
--- a/src/Pure/General/yxml.ML	Tue Jul 12 15:17:37 2011 +0200
+++ b/src/Pure/General/yxml.ML	Tue Jul 12 15:32:16 2011 +0200
@@ -15,6 +15,8 @@
 
 signature YXML =
 sig
+  val X: Symbol.symbol
+  val Y: Symbol.symbol
   val embed_controls: string -> string
   val detect: string -> bool
   val output_markup: Markup.T -> string * string
@@ -45,8 +47,8 @@
 
 (* markers *)
 
-val X = Symbol.ENQ;
-val Y = Symbol.ACK;
+val X = chr 5;
+val Y = chr 6;
 val XY = X ^ Y;
 val XYX = XY ^ X;