# HG changeset patch
# User berghofe
# Date 1210150785 -7200
# Node ID 7b7139f961bd96e031c52e1c3a70b3c27dcc61cc
# Parent  229e8078b1e0d9026d6540a1391a1a39577ddc6d
Replaced Pattern.eta_contract_atom by Envir.eta_contract.

diff -r 229e8078b1e0 -r 7b7139f961bd src/FOLP/hypsubst.ML
--- 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