changeset 56458 | a8d960baa5c2 |
parent 56447 | 1e77ed11f2f7 |
child 56616 | abc2da18d08d |
--- a/src/Pure/PIDE/protocol.ML Mon Apr 07 21:23:02 2014 +0200 +++ b/src/Pure/PIDE/protocol.ML Mon Apr 07 23:02:29 2014 +0200 @@ -34,7 +34,7 @@ YXML.parse_body blobs_yxml |> let open XML.Decode in list (variant - [fn ([], a) => Exn.Res (triple string string (option string) a), + [fn ([], a) => Exn.Res (pair string (option string) a), fn ([], a) => Exn.Exn (ERROR (string a))]) end; in