# HG changeset patch
# User paulson
# Date 855913223 -3600
# Node ID 704b6c7432cff4f960b56ad616f31f1a6b3a11ac
# Parent  99df9182f5a5f8cc60f788d5281b76d8f4333d42
A bit more pattern-matching in eta_contract

diff -r 99df9182f5a5 -r 704b6c7432cf src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Fri Feb 14 10:38:48 1997 +0100
+++ b/src/Pure/pattern.ML	Fri Feb 14 10:40:23 1997 +0100
@@ -223,10 +223,10 @@
 
 (*Perform eta-contractions upon a term*)
 fun eta_contract (Abs(a,T,body)) = 
-      (case eta_contract body  of
-        body' as (f $ Bound i) => 
-	  if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f 
-	  else 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')
+	  else incr_boundvars ~1 f 
       | body' => Abs(a,T,body'))
   | eta_contract(f$t) = eta_contract f $ eta_contract t
   | eta_contract t = t;