[isabelle] Bizarre type unification error

In the attached proof script, I receive the following message after
loading the buffer into Isabelle:

*** Type unification failed
*** Type error in application: Incompatible operand type
*** Operator:  Cl_P :: 'a set => 'a set
*** Operand:   T :: ??'a llist set
*** At command "assume".

I expect these types to be unifiable.  Should not "??'a llist set"
unify with "'a set" such that "??'a llist = 'a"?

I'm attempting to use a set of functions out of which I'm going to
pick an arbitrary function and invoke the only property I know about
it (namely, that it's monotonic; see the definition Cls).  What have I
done wrong?

The proof script depends on the LList2 library, available on AFP


Attachment: Error.thy
Description: Binary data

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.