fixed bug
authorhaftmann
Fri Oct 13 16:52:48 2006 +0200 (2006-10-13)
changeset 21013b9321724c2cc
parent 21012 f08574148b7a
child 21014 3b0c2641f740
fixed bug
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Fri Oct 13 16:52:47 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Oct 13 16:52:48 2006 +0200
     1.3 @@ -799,7 +799,7 @@
     1.4        | strip_abs (Abs (v, T, t)) (k, used) =
     1.5            let
     1.6              val ([v'], used') = Name.variants [v] used;
     1.7 -            val t' = subst_bound (Free (v, T), t);
     1.8 +            val t' = subst_bound (Free (v', T), t);
     1.9              val ((vs, t''), (k', used'')) = strip_abs t' (k - 1, used');
    1.10            in (((v', T) :: vs, t''), (k', used'')) end
    1.11        | strip_abs t (k, used) = (([], t), (k, used));