src/Pure/pattern.ML
changeset 2792 6c17c5ec3d8b
parent 2751 673c4eefd2e1
child 4667 6328d427a339
     1.1 --- a/src/Pure/pattern.ML	Tue Mar 11 17:20:59 1997 +0100
     1.2 +++ b/src/Pure/pattern.ML	Fri Mar 14 10:35:30 1997 +0100
     1.3 @@ -226,21 +226,51 @@
     1.4  
     1.5  
     1.6  (*Eta-contract a term (fully)*)
     1.7 +
     1.8 +(* copying: *)
     1.9  fun eta_contract (Abs(a,T,body)) = 
    1.10        (case  eta_contract body  of
    1.11          body' as (f $ Bound 0) => 
    1.12 -	  if (0 mem_int loose_bnos f) then Abs(a,T,body')
    1.13 +	  if loose_bvar1(f,0) 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;
    1.18  
    1.19  
    1.20 +(* sharing:
    1.21 +local
    1.22 +
    1.23 +fun eta(Abs(x,T,t)) =
    1.24 +     (case eta t of
    1.25 +        None => (case t of
    1.26 +                   f $ Bound 0 => if loose_bvar1(f,0)
    1.27 +                                  then None
    1.28 +                                  else Some(incr_boundvars ~1 f)
    1.29 +                 | _ => None)
    1.30 +      | Some(t') => (case t' of
    1.31 +                       f $ Bound 0 => if loose_bvar1(f,0)
    1.32 +                                      then Some(Abs(x,T,t'))
    1.33 +                                      else Some(incr_boundvars ~1 f)
    1.34 +                     | _ => Some(Abs(x,T,t'))))
    1.35 +  | eta(s$t) = (case (eta s,eta t) of
    1.36 +                  (None,   None)    => None
    1.37 +                | (None,   Some t') => Some(s  $ t')
    1.38 +                | (Some s',None)    => Some(s' $ t)
    1.39 +                | (Some s',Some t') => Some(s' $ t'))
    1.40 +  | eta _ = None
    1.41 +
    1.42 +in
    1.43 +
    1.44 +fun eta_contract t = case eta t of None => t | Some(t') => t';
    1.45 +
    1.46 +end; *)
    1.47 +
    1.48  (*Eta-contract a term from outside: just enough to reduce it to an atom*)
    1.49  fun eta_contract_atom (t0 as Abs(a, T, body)) = 
    1.50        (case  eta_contract2 body  of
    1.51          body' as (f $ Bound 0) => 
    1.52 -	    if (0 mem_int loose_bnos f) then Abs(a,T,body')
    1.53 +	    if loose_bvar1(f,0) then Abs(a,T,body')
    1.54  	    else eta_contract_atom (incr_boundvars ~1 f)
    1.55        | _ => t0)
    1.56    | eta_contract_atom t = t