[isabelle-dev] auto raises a TYPE exception
makarius at sketis.net
Tue May 28 18:50:17 CEST 2013
On Tue, 28 May 2013, Lawrence Paulson wrote:
> the disagreement pairs should be fully eta-expanded by this point,
> though I haven't looked at the code recently. That would imply that the
> body_type cannot be a function type.
Can you look now? Notably in Isabelle/3b9c31867707, and the parent of it.
So far the summary of this thread:
* There is nothing wrong with Thm.assumption/Thm.bicompose_aux, as
suspected by Stefan. The non-incrementing of Vars is just a
consequence of Thm.compose_no_flatten used in SELECT_GOAL. (The use
of compose here goes back to Stefan himself from 2001.)
* Some indication that extra type variables in subterms are not fully
taken care of.
More information about the isabelle-dev