changeset 21013 | b9321724c2cc |
parent 20854 | f9cf9e62d11c |
child 21353 | cfee13454195 |
--- 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));