# HG changeset patch # User wenzelm # Date 1310505634 -7200 # Node ID 321ebd0518974e7c5fc35aa092139af11eb100c7 # Parent e84239a47f323aab1ce549d92f8f94c19260649a tuned; diff -r e84239a47f32 -r 321ebd051897 src/Pure/term_xml.ML --- a/src/Pure/term_xml.ML Tue Jul 12 20:53:14 2011 +0200 +++ b/src/Pure/term_xml.ML Tue Jul 12 23:20:34 2011 +0200 @@ -29,7 +29,7 @@ val sort = list string; fun typ T = T |> variant - [fn Type (a, b) => ([a], (list typ) b), + [fn Type (a, b) => ([a], list typ b), fn TFree (a, b) => ([a], sort b), fn TVar ((a, b), c) => ([a, int_atom b], sort c)]; @@ -39,7 +39,7 @@ fn Var ((a, b), c) => ([a, int_atom b], typ c), fn Bound a => ([int_atom a], []), fn Abs (a, b, c) => ([a], pair typ term (b, c)), - fn a $ b => ([], pair term term (a, b))]; + fn op $ a => ([], pair term term a)]; end;