On 18 Jan 2011, at 14:40, Roger Bishop Jones wrote:
> I am finding that if I give something the status of a binder
> before defining the constant, so that it can be used as a
> binder in the definition, the definition fails.
> The error message alleges that the binder occurs freely in
> the definition (which I suppose is true).
> Is this a known feature?
It is due to a bug in type inference that I fixed some time ago, but my plans
for an OpenProofPower release in the second half of 2010 went awry. I plan a
release including all the outstanding bug fixes and one or two minor new
features before the end of January.
> Roger Jones
> Proofpower mailing list
Proofpower mailing list