[isabelle-dev] auto raises a TYPE exception

[Stefan Berghofer]

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