[isabelle] A type unification error

Dear all:

I'm trying your tutorial material on SAT  solver (page 196).

   I meet a type error that I cannot solve. Could you please do me
   a hand?
   see line 64 in the attachment.

The error says that Isabelle cannot unify the same type .


Attachment: machineLearning.thy
Description: Binary data

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