[isabelle-dev] Variable "?n" has two distinct types

[Gerwin Klein]

I've managed to get the following error message with Isabelle2011 when running simp:

*** exception TYPE raised (line 109 of "envir.ML"): Variable "?n" has two distinct types
*** At command "apply" (line 14 of "/Users/kleing/Simp.thy")

The end of the simplifier trace shows this rule being produced, which indeed has "?n" with different types:

[1]Procedure "defined EX" produced rewrite rule:
\<exists>x. ?n (?p S) = Some x \<and> ?n S = x \<equiv> \<exists>x. ?n S = x \<and> ?n (?p S) = Some x

I've distilled the problem into the attached small theory. The trigger seems to be that "n" occurs as Free in the goal and as a (completely different) Var ?n in lemma P. This does not seem to trigger if there are no parameters around in the goal (hence the forall in the example).

The workaround was to avoid the simplifier until ?n is instantiated, but that's a hack, of course.

Cheers,
Gerwin

-------------- next part --------------
A non-text attachment was scrubbed...
Name: Simp.thy
Type: application/octet-stream
Size: 245 bytes
Desc: not available
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20110206/4e240410/attachment.obj>