[isabelle-dev] auto raises a TYPE exception

Stefan Berghofer 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 mailing list