use eta-contracted version for occurrence check (avoids possible non-termination)
Test case: lemma "fwrap f = (%v. f v) ==> P f" apply clarify;
pointed out by Thomas Sewell

--- a/src/Provers/hypsubst.ML	Fri Sep 10 15:55:09 2010 +0200
+++ b/src/Provers/hypsubst.ML	Fri Sep 10 23:56:35 2010 +0200
@@ -115,11 +115,11 @@
      | (_, Bound i) => if loose(i,t) orelse novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)
-     | (Free _, _) =>  if bnd orelse Logic.occs(t,u) orelse
+     | (t' as Free _, _) => if bnd orelse Logic.occs(t',u) orelse
                           novars andalso has_vars u
                        then raise Match
                        else true                (*eliminates t*)
-     | (_, Free _) =>  if bnd orelse Logic.occs(u,t) orelse
+     | (_, u' as Free _) => if bnd orelse Logic.occs(u',t) orelse
                           novars andalso has_vars t
                        then raise Match
                        else false               (*eliminates u*)