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