src/Pure/General/yxml.ML
changeset 38266 492d377ecfe2
parent 38265 cc9fde54311f
child 38474 e498dc2eb576
     1.1 --- a/src/Pure/General/yxml.ML	Tue Aug 10 20:13:52 2010 +0200
     1.2 +++ b/src/Pure/General/yxml.ML	Tue Aug 10 22:26:23 2010 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4    val output_markup: Markup.T -> string * string
     1.5    val element: string -> XML.attributes -> string list -> string
     1.6    val string_of: XML.tree -> string
     1.7 -  val parse_body: string -> XML.tree list
     1.8 +  val parse_body: string -> XML.body
     1.9    val parse: string -> XML.tree
    1.10  end;
    1.11