Fixed bug in eta_long.

--- a/src/HOL/Integ/presburger.ML	Fri Apr 04 17:00:25 2003 +0200
+++ b/src/HOL/Integ/presburger.ML	Fri Apr 04 17:01:12 2003 +0200
@@ -68,9 +68,12 @@
   | 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))
-      in list_abs (map (pair "x") Us, Unify.combound
-        (list_comb (u, map (eta_long Ts) ts), 0, length Us))
+      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);
 
 (* Some Types*)

--- a/src/HOL/Tools/Presburger/presburger.ML	Fri Apr 04 17:00:25 2003 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML	Fri Apr 04 17:01:12 2003 +0200
@@ -68,9 +68,12 @@
   | 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))
-      in list_abs (map (pair "x") Us, Unify.combound
-        (list_comb (u, map (eta_long Ts) ts), 0, length Us))
+      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);
 
 (* Some Types*)