That mysterious type always throws me. I guess you are saying that this dangling type dependence introduces a function type in the first line. Unfortunately, this is a difficult matter to explain to a student. I'll just have to tell him to constrain the types of his bound variables. I believe that the type of X may also be to blame.
Larry On 26 Feb 2013, at 16:27, Tobias Nipkow <[email protected]> wrote: > The two y's are given separate types. In fact, Isabelle introduces ??'a itself > in the process. _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
