src/Pure/Thy/thy_header.scala
changeset 43724 4e58485fa320
parent 43723 8a63c95b1d5b
child 43725 bebcfcad12d4
     1.1 --- a/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:00:22 2011 +0200
     1.2 +++ b/src/Pure/Thy/thy_header.scala	Sun Jul 10 13:51:21 2011 +0200
     1.3 @@ -32,9 +32,8 @@
     1.4    }
     1.5  
     1.6    def make_xml_data(header: Header): XML.Body =
     1.7 -    XML_Data.make_triple(XML_Data.make_string,
     1.8 -      XML_Data.make_list(XML_Data.make_string),
     1.9 -        XML_Data.make_list(XML_Data.make_string))(header.name, header.imports, header.uses)
    1.10 +  { import XML_Data.Make._
    1.11 +    triple(string, list(string), list(string))(header.name, header.imports, header.uses) }
    1.12  
    1.13  
    1.14    /* file name */