--- 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!
*)