src/Pure/Thy/thy_header.scala
changeset 43725 bebcfcad12d4
parent 43724 4e58485fa320
child 43731 70072780e095
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 15:48:15 2011 +0200
     1.3 @@ -31,9 +31,12 @@
     1.4        Header(f(name), imports.map(f), uses.map(f))
     1.5    }
     1.6  
     1.7 -  def make_xml_data(header: Header): XML.Body =
     1.8 -  { import XML_Data.Make._
     1.9 -    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
    1.10 +  val make_xml_data: XML_Data.Make.T[Header] =
    1.11 +  {
    1.12 +    case Header(name, imports, uses) =>
    1.13 +      import XML_Data.Make._
    1.14 +      triple(string, list(string), list(string))(name, imports, uses)
    1.15 +  }
    1.16  
    1.17  
    1.18    /* file name */