src/Pure/pattern.ML
changeset 2616 704b6c7432cf
parent 2227 18e993700540
child 2725 9453616d4b80
     1.1 --- a/src/Pure/pattern.ML	Fri Feb 14 10:38:48 1997 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Feb 14 10:40:23 1997 +0100
     1.3 @@ -223,10 +223,10 @@
     1.4  
     1.5  (*Perform eta-contractions upon a term*)
     1.6  fun eta_contract (Abs(a,T,body)) = 
     1.7 -      (case eta_contract body  of
     1.8 -        body' as (f $ Bound i) => 
     1.9 -	  if i=0 andalso not (0 mem_int loose_bnos f) then incr_boundvars ~1 f 
    1.10 -	  else Abs(a,T,body')
    1.11 +      (case  eta_contract body  of
    1.12 +        body' as (f $ Bound 0) => 
    1.13 +	  if (0 mem_int loose_bnos f) then Abs(a,T,body')
    1.14 +	  else incr_boundvars ~1 f 
    1.15        | body' => Abs(a,T,body'))
    1.16    | eta_contract(f$t) = eta_contract f $ eta_contract t
    1.17    | eta_contract t = t;