# HG changeset patch
# User krauss
# Date 1284155795 -7200
# Node ID 4f9e933a16e2aab480c2ace959c0810b9b5404e7
# Parent  635e09dea4655470720e8714a5e54b984ca4d888
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

diff -r 635e09dea465 -r 4f9e933a16e2 src/Provers/hypsubst.ML
--- 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*)