[Agda] LaTeX-Backend: \renewcommand{\defaultcolumn}{...} shows no effect

[Andreas Abel]

Hi to the users of Agda's LaTeX-Backend,

this is a very nice tool, I am using it for the first time.

I found the space between the columns excessive.  After some research I 
found

   \defaultcolumn{l}

in agda.sty.  I tried the following

   \usepackage{latex/agda}
   \renewcommand{\defaultcolumn}{@{~}l@{~}}

but to no avail.  By chance I found out that if I modify the command in 
agda.sty, to

   \defaultcolumn{@{~}l@{~}}

everything works as excepted.

Why did \renewcommand{...} show no effect?  (I always thought that LaTeX 
has dynamic binding...)

Cheers,
Andreas