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