Term.has_abs;
authorwenzelm
Fri Sep 21 22:51:10 2007 +0200 (2007-09-21)
changeset 246709aae962b1d56
parent 24669 4579eac2c997
child 24671 35075a1e9599
Term.has_abs;
src/Pure/envir.ML
     1.1 --- a/src/Pure/envir.ML	Fri Sep 21 22:51:08 2007 +0200
     1.2 +++ b/src/Pure/envir.ML	Fri Sep 21 22:51:10 2007 +0200
     1.3 @@ -238,14 +238,10 @@
     1.4    | eta _ = raise SAME
     1.5  and etah t = (eta t handle SAME => t);
     1.6  
     1.7 -fun has_abs (Abs _) = true
     1.8 -  | has_abs (t $ u) = has_abs t orelse has_abs u
     1.9 -  | has_abs _ = false;
    1.10 -
    1.11  in
    1.12  
    1.13  fun eta_contract t =
    1.14 -  if has_abs t then etah t else t;
    1.15 +  if Term.has_abs t then etah t else t;
    1.16  
    1.17  val beta_eta_contract = eta_contract o beta_norm;
    1.18