# HG changeset patch
# User paulson
# Date 857552912 -3600
# Node ID df3a269b6f34d60cf3febccee2ad3135356bf760
# Parent  230f2643107eeafef1c3e57fa97f0affcc39a034
Now uses eta_contract_atom for greater speed

diff -r 230f2643107e -r df3a269b6f34 src/FOLP/hypsubst.ML
--- a/src/FOLP/hypsubst.ML	Wed Mar 05 10:07:04 1997 +0100
+++ b/src/FOLP/hypsubst.ML	Wed Mar 05 10:08:32 1997 +0100
@@ -42,7 +42,7 @@
   It's not safe to substitute for a variable free in the premises,
     but how could we check for this?*)
 fun inspect_pair bnd (t,u) =
-  case (Pattern.eta_contract t, Pattern.eta_contract u) of
+  case (Pattern.eta_contract_atom t, Pattern.eta_contract_atom u) of
        (Bound i, _) => if loose(i,u) then raise Match 
                        else sym         (*eliminates t*)
      | (_, Bound i) => if loose(i,t) then raise Match