[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 19:03:10 CEST 2013
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
> invoking Thm.compose_no_flatten? A similar approach is also used in
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.
More information about the isabelle-dev