[Agda] Failed type checking of standard lib after removed eta-contraction of function bodies in `Def.hs'

[Dirk Ullrich]

Hi all,
 when I try to generate all `agdai' files for the Agda standard lib at
once with the current Agda version from darcs repository I get an
error for `Data.Star.Decoration.agda':
...
.../Data/Star/Decoration.agda:54,15-16
xs != ε of type Star (λ .i' .j → T .i' .j) j j
when checking that the pattern ε has type
Star (DecoratedWith (λ {.i} {.j} → P)) (nonEmpty xs) (nonEmpty ε)

Here it is caused by Andreas' patch that removes eta-contraction of
function bodies in `Def.hs'.

Can anyone reproduce this?

Dirk