# 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