Re: Unification/coercion failure

[Chris Warburton]

Closed. This turns out to be a problem with how we were rendering the
'undefined cases'. We were doing things like:

    destructor-foo(Bar(free1, free2))

Yet this is nonsense, since Isabelle doesn't use 'f(x, y)' notation for
calling functions; it uses juxtaposition. Hence we were forming tuples
of free variables, which don't have the correct type.

Fixed now, by ditching the commas and moving the parentheses:

    destructor-foo (Bar free1 free2)