[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Stefan Berghofer wrote:

> On 05/28/2013 02:32 PM, Makarius wrote:
>> The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which is 
>> the basis of SELECT_GOAL).
>> 
>> This explains why there is no extra incrementing of Vars, unlike the normal 
>> resolution-family of operations.
>
> So what would be wrong with applying Thm.incr_indexes to st' in Goal.retrofit 
> before
> invoking Thm.compose_no_flatten? A similar approach is also used in 
> Drule.comp_no_flatten.

Shifting indexes will confuse many proof tools, it can take quite a long 
time to change that substantially.

The idea that "comp" would do that without incrementing is not a recent 
add-on, we have been following that approach for approx. 15 years.


So maybe we can enter round 4--7 of investigation, to see if anything 
needs to be added or subtracted from 3b9c31867707.


 	Makarius