[isabelle-dev] auto raises a TYPE exception

Makarius 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 mailing list