# HG changeset patch
# User berghofe
# Date 1049468472 -7200
# Node ID 4ac9d55573da86d0cea6da2abd909db9c37bca74
# Parent  ae9a2a433388979757b4006f4d6f070cced9741b
Fixed bug in eta_long.

diff -r ae9a2a433388 -r 4ac9d55573da src/HOL/Integ/presburger.ML
--- 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*)
diff -r ae9a2a433388 -r 4ac9d55573da src/HOL/Tools/Presburger/presburger.ML
--- 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*)