[isabelle-dev] auto raises a TYPE exception

[Stefan Berghofer]

On 05/27/2013 05:26 PM, Makarius wrote:
> Anyway, after 2-3 more rounds of investigation, I've found more profound weaknesses of pattern.ML and unify.ML concerning unification of types. This could lead to situations as sketched above, where types of variables were not properly instantiated.  E.g. here:
>
> [...]
>
>
> The following change addresses that, although I do not claim to "fix" anything -- it is even more critical as usual, since it affects operations of the inference kernel.

Hi Markus,

I do not quite understand the rationale behind this change. As I pointed out in my previous mail,
it is an error to supply disagreement pairs to unify containing Vars that have the same name but
different types. So I don't think one should change pattern.ML and unify.ML so that it unifies
these different types and pretends that everything is all right, but one should find and correct
the function that supplies these erroneous disagreement pairs to unify. Do we have an idea where
these disagreement pairs came from? Maybe someone just forgot to increment the indices of variables
before invoking bicompose?

Greetings,
Stefan