# HG changeset patch
# User wenzelm
# Date 1190407870 -7200
# Node ID 9aae962b1d5675c4f0107e7f6255a665837ab7db
# Parent  4579eac2c997db3860b9fda7bf91bdda448bcb95
Term.has_abs;

diff -r 4579eac2c997 -r 9aae962b1d56 src/Pure/envir.ML
--- a/src/Pure/envir.ML	Fri Sep 21 22:51:08 2007 +0200
+++ b/src/Pure/envir.ML	Fri Sep 21 22:51:10 2007 +0200
@@ -238,14 +238,10 @@
   | eta _ = raise SAME
 and etah t = (eta t handle SAME => t);
 
-fun has_abs (Abs _) = true
-  | has_abs (t $ u) = has_abs t orelse has_abs u
-  | has_abs _ = false;
-
 in
 
 fun eta_contract t =
-  if has_abs t then etah t else t;
+  if Term.has_abs t then etah t else t;
 
 val beta_eta_contract = eta_contract o beta_norm;