src/Pure/term_xml.ML
changeset 43767 e0219ef7f84c
parent 43731 70072780e095
child 43778 ce9189450447
     1.1 --- a/src/Pure/term_xml.ML	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/Pure/term_xml.ML	Tue Jul 12 10:44:30 2011 +0200
     1.3 @@ -15,8 +15,8 @@
     1.4  
     1.5  signature TERM_XML =
     1.6  sig
     1.7 -  structure Encode: TERM_XML_OPS where type 'a T = 'a XML_Data.Encode.T
     1.8 -  structure Decode: TERM_XML_OPS where type 'a T = 'a XML_Data.Decode.T
     1.9 +  structure Encode: TERM_XML_OPS where type 'a T = 'a XML.Encode.T
    1.10 +  structure Decode: TERM_XML_OPS where type 'a T = 'a XML.Decode.T
    1.11  end;
    1.12  
    1.13  structure Term_XML: TERM_XML =
    1.14 @@ -27,7 +27,7 @@
    1.15  structure Encode =
    1.16  struct
    1.17  
    1.18 -open XML_Data.Encode;
    1.19 +open XML.Encode;
    1.20  
    1.21  val indexname = pair string int;
    1.22  
    1.23 @@ -54,7 +54,7 @@
    1.24  structure Decode =
    1.25  struct
    1.26  
    1.27 -open XML_Data.Decode;
    1.28 +open XML.Decode;
    1.29  
    1.30  val indexname = pair string int;
    1.31