Replaced Pattern.eta_contract_atom by Envir.eta_contract.

--- a/src/FOLP/hypsubst.ML	Wed May 07 10:59:44 2008 +0200
+++ b/src/FOLP/hypsubst.ML	Wed May 07 10:59:45 2008 +0200
@@ -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_atom t, Pattern.eta_contract_atom u) of
+  case (Envir.eta_contract t, Envir.eta_contract u) of
        (Bound i, _) => if loose(i,u) then raise Match 
                        else sym         (*eliminates t*)
      | (_, Bound i) => if loose(i,t) then raise Match