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