diff -r 9545bb3cefac -r e0219ef7f84c src/Pure/term_xml.ML
--- a/src/Pure/term_xml.ML	Tue Jul 12 16:00:05 2011 +0900
+++ b/src/Pure/term_xml.ML	Tue Jul 12 10:44:30 2011 +0200
@@ -15,8 +15,8 @@
 
 signature TERM_XML =
 sig
-  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
-  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
+  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
+  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
 end;
 
 structure Term_XML: TERM_XML =
@@ -27,7 +27,7 @@
 structure Encode =
 struct
 
-open XML_Data.Encode;
+open XML.Encode;
 
 val indexname = pair string int;
 
@@ -54,7 +54,7 @@
 structure Decode =
 struct
 
-open XML_Data.Decode;
+open XML.Decode;
 
 val indexname = pair string int;