diff -r b65da0c53d94 -r 6c17c5ec3d8b src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Tue Mar 11 17:20:59 1997 +0100
+++ b/src/Pure/pattern.ML	Fri Mar 14 10:35:30 1997 +0100
@@ -226,21 +226,51 @@
 
 
 (*Eta-contract a term (fully)*)
+
+(* copying: *)
 fun eta_contract (Abs(a,T,body)) = 
       (case  eta_contract body  of
         body' as (f $ Bound 0) => 
-	  if (0 mem_int loose_bnos f) then Abs(a,T,body')
+	  if loose_bvar1(f,0) then Abs(a,T,body')
 	  else incr_boundvars ~1 f 
       | body' => Abs(a,T,body'))
   | eta_contract(f$t) = eta_contract f $ eta_contract t
   | eta_contract t = t;
 
 
+(* sharing:
+local
+
+fun eta(Abs(x,T,t)) =
+     (case eta t of
+        None => (case t of
+                   f $ Bound 0 => if loose_bvar1(f,0)
+                                  then None
+                                  else Some(incr_boundvars ~1 f)
+                 | _ => None)
+      | Some(t') => (case t' of
+                       f $ Bound 0 => if loose_bvar1(f,0)
+                                      then Some(Abs(x,T,t'))
+                                      else Some(incr_boundvars ~1 f)
+                     | _ => Some(Abs(x,T,t'))))
+  | eta(s$t) = (case (eta s,eta t) of
+                  (None,   None)    => None
+                | (None,   Some t') => Some(s  $ t')
+                | (Some s',None)    => Some(s' $ t)
+                | (Some s',Some t') => Some(s' $ t'))
+  | eta _ = None
+
+in
+
+fun eta_contract t = case eta t of None => t | Some(t') => t';
+
+end; *)
+
 (*Eta-contract a term from outside: just enough to reduce it to an atom*)
 fun eta_contract_atom (t0 as Abs(a, T, body)) = 
       (case  eta_contract2 body  of
         body' as (f $ Bound 0) => 
-	    if (0 mem_int loose_bnos f) then Abs(a,T,body')
+	    if loose_bvar1(f,0) then Abs(a,T,body')
 	    else eta_contract_atom (incr_boundvars ~1 f)
       | _ => t0)
   | eta_contract_atom t = t