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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
