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