[isabelle-dev] auto raises a TYPE exception

[Makarius]

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