blanchet [Thu, 24 Jun 2010 17:27:18 +0200] rev 37540
better eta-expansion in Sledgehammer's clausification;
make the eta-expansion code more robust in the face of polymorphic arguments + make eta-expansion happen more often, since it first-orderizes things