src/Pure/Thy/thy_header.scala
changeset 43767 e0219ef7f84c
parent 43731 70072780e095
child 44157 a21d3e1e64fd
     1.1 --- a/src/Pure/Thy/thy_header.scala	Tue Jul 12 16:00:05 2011 +0900
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Tue Jul 12 10:44:30 2011 +0200
     1.3 @@ -31,10 +31,10 @@
     1.4        Header(f(name), imports.map(f), uses.map(f))
     1.5    }
     1.6  
     1.7 -  val encode_xml_data: XML_Data.Encode.T[Header] =
     1.8 +  val xml_encode: XML.Encode.T[Header] =
     1.9    {
    1.10      case Header(name, imports, uses) =>
    1.11 -      import XML_Data.Encode._
    1.12 +      import XML.Encode._
    1.13        triple(string, list(string), list(string))(name, imports, uses)
    1.14    }
    1.15