# HG changeset patch
# User berghofe
# Date 1052592782 -7200
# Node ID 75a399c2781f3bed084cf9110fcb5590e357c605
# Parent  3d53dcd7787731a0b0f231155db2005625886fd5
Added new function eta_long.

diff -r 3d53dcd77877 -r 75a399c2781f src/Pure/pattern.ML
--- a/src/Pure/pattern.ML	Sat May 10 20:52:18 2003 +0200
+++ b/src/Pure/pattern.ML	Sat May 10 20:53:02 2003 +0200
@@ -22,6 +22,7 @@
   val trace_unify_fail  : bool ref
   val aeconv            : term * term -> bool
   val eta_contract      : term -> term
+  val eta_long          : typ list -> term -> term
   val beta_eta_contract : term -> term
   val eta_contract_atom : term -> term
   val match             : type_sig -> term * term
@@ -328,6 +329,19 @@
 and eta_contract2 (f$t) = f $ eta_contract_atom t
   | eta_contract2 t     = eta_contract_atom t;
 
+(* put a term into eta long beta normal form *)
+fun eta_long Ts (Abs (s, T, t)) = Abs (s, T, eta_long (T :: Ts) t)
+  | eta_long Ts t = (case strip_comb t of
+      (Abs _, _) => eta_long Ts (Envir.beta_norm t)
+    | (u, ts) => 
+      let
+        val Us = binder_types (fastype_of1 (Ts, t));
+        val i = length Us
+      in list_abs (map (pair "x") Us,
+        list_comb (incr_boundvars i u, map (eta_long (rev Us @ Ts))
+          (map (incr_boundvars i) ts @ map Bound (i - 1 downto 0))))
+      end);
+
 
 (*Tests whether 2 terms are alpha/eta-convertible and have same type.
   Note that Consts and Vars may have more than one type.*)