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