Re: "UnequalLengths" error

[Chris Warburton]

I've added a test to check that the names, taken in order, from the
'functions' value match those of the 'definitions' derivation.

To ensure this, I've changed the way that we calculate the
definitions. First we calculate all definitions, up front, from the
'A.thy' file. Then, we look up each definition in order.

This has exposed a problem, that there are things in 'functions' which
aren't in 'definitions'. It looks like these are from mutually-recursive
definitions, e.g. 'foo :: bar and baz :: quux ...'