# HG changeset patch
# User haftmann
# Date 1160751168 -7200
# Node ID b9321724c2ccbe2551debb675ad51bffa86d66a6
# Parent  f08574148b7a0180e78eb03af27f34e92e6dbd2a
fixed bug

diff -r f08574148b7a -r b9321724c2cc src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Oct 13 16:52:47 2006 +0200
+++ b/src/Pure/term.ML	Fri Oct 13 16:52:48 2006 +0200
@@ -799,7 +799,7 @@
       | strip_abs (Abs (v, T, t)) (k, used) =
           let
             val ([v'], used') = Name.variants [v] used;
-            val t' = subst_bound (Free (v, T), t);
+            val t' = subst_bound (Free (v', T), t);
             val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
           in (((v', T) :: vs, t''), (k', used'')) end
       | strip_abs t (k, used) = (([], t), (k, used));