# HG changeset patch
# User wenzelm
# Date 1011216226 -3600
# Node ID f76180d14819734aa656b13f0b5ced1eaee47c2c
# Parent  6b41c750451cee330a3b6401c4e05f5e0360f726
added beta_eta_contract;

diff -r 6b41c750451c -r f76180d14819 src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Wed Jan 16 21:01:08 2002 +0100
+++ b/src/Pure/pattern.ML	Wed Jan 16 22:23:46 2002 +0100
@@ -21,6 +21,7 @@
   type env
   val aeconv            : term * term -> bool
   val eta_contract      : term -> term
+  val beta_eta_contract : term -> term
   val eta_contract_atom : term -> term
   val match             : type_sig -> term * term
                           -> (indexname*typ)list * (indexname*term)list
@@ -236,6 +237,8 @@
   | eta_contract(f$t) = eta_contract f $ eta_contract t
   | eta_contract t = t;
 
+val beta_eta_contract = eta_contract o Envir.beta_norm;
+
 (*Eta-contract a term from outside: just enough to reduce it to an atom
 DOESN'T QUITE WORK!
 *)