[isabelle-dev] auto raises a TYPE exception

[Makarius]

On Tue, 28 May 2013, Makarius wrote:

> The crash happens in Thm.bicompose_no_flatten (via Goal.retrofit, which 
> is the basis of SELECT_GOAL).

This also touches the still open thread on SELECT_GOAL here 
https://lists.cam.ac.uk/mailman/htdig/cl-isabelle-users/2013-March/msg00118.html 
although that was about term variables, not type variables.


 	Makarius