src/Pure/Thy/thy_header.scala
changeset 43731 70072780e095
parent 43725 bebcfcad12d4
child 43767 e0219ef7f84c
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 17:58:11 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 20:59:04 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 make_xml_data: XML_Data.Make.T[Header] =
     1.8 +  val encode_xml_data: XML_Data.Encode.T[Header] =
     1.9    {
    1.10      case Header(name, imports, uses) =>
    1.11 -      import XML_Data.Make._
    1.12 +      import XML_Data.Encode._
    1.13        triple(string, list(string), list(string))(name, imports, uses)
    1.14    }
    1.15