[isabelle-dev] auto raises a TYPE exception
berghofe at in.tum.de
Tue May 28 18:50:07 CEST 2013
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.
More information about the isabelle-dev