<br><br><div class="gmail_quote">On Fri, Dec 11, 2009 at 16:17, Matthew Flatt <span dir="ltr">&lt;<a href="mailto:mflatt@cs.utah.edu">mflatt@cs.utah.edu</a>&gt;</span> wrote:<br><blockquote class="gmail_quote" style="border-left: 1px solid rgb(204, 204, 204); margin: 0pt 0pt 0pt 0.8ex; padding-left: 1ex;">


Note that the error message above is specifically about the external<br>
name.<br></blockquote></div><br>Oh, so that is why. Thanks. I can (re-)*wire my brain in a more decent way.<br>