[isabelle-dev] internal TYPE exception at lemma statement

[Alexander Krauss]

Dear all,

To avoid that this issue, encountered by Lars, gets lost, I'll re-raise 
it here:

The following lemma statement raises an obscure internal TYPE exception:

lemma
   assumes "P foo" (is "P ?bar")
   shows "Q ?bar"

I assume that is-bindings cannot be used in the same structured 
statement. I also assume that this would be hard to support in general.

Is there any chance of getting a decent error message here, since it is 
actually quite natural to attempt something like this.

Alex