Re: "UnequalLengths" error

[Chris Warburton]

Looks like this is due to zipping up functions with their definitions.

The exception trace points us to Pure/library.thy, which contains this:

    (*combine two lists forming a list of pairs:
      [x1, ..., xn] ~~ [y1, ..., yn]  ===>  [(x1, y1), ..., (xn, yn)]*)
    fun [] ~~ [] = []
      | (x :: xs) ~~ (y :: ys) = (x, y) :: (xs ~~ ys)
      | _ ~~ _ = raise ListPair.UnequalLengths;

This is used in isacosy-template.thy in the following way:

    val fundefs = functions ~~ def_thrms;

Hence 'functions' and 'def_thrms' need to be the same length in order
for the zip to work.