20070821-1

When refining a goal, the given term sometimes loses parentheses when it is inserted in the buffer.

As a trivial example, consider the function foo : (A : Set) -> (f : A -> A) -> A -> A.

I first define it as foo A f x = ? and then type check. When I refine with f (f x), Agda inserts f f x into the buffer instead, which is, of course, not correct.

Fixed. -- Ulf