[Agda] beamer + latex mode + font sizes

[Jacques Carette]

I am trying to control the font size of agda code block in .lagda files 
in a beamer presentation, and not succeeding.

I have tried:
1. using
{\tiny{
\begin{code}
...
\end{code}}}

2. changing the lines
\newcommand{\AgdaCodeStyle}{}
% \newcommand{\AgdaCodeStyle}{\tiny}
to
% \newcommand{\AgdaCodeStyle}{}
\newcommand{\AgdaCodeStyle}{\tiny}
in agda.sty

And neither seem to have had any effect.  Oddly, I have been able to 
change \mathindent successfully to have less indent.

I use
agda --allow-unsolved-metas --latex -i . -i $(AGDALIB) -i $(CATLIB) 
slides.lagda
pdflatex latex/slides.tex
which otherwise works like a charm, except for this.

What am I missing?

Jacques