changeset 4502 | 337c073de95e |
parent 2525 | 477c05586286 |
child 5184 | 9b8547a9496a |
--- a/src/HOL/MiniML/W.thy Mon Dec 29 21:39:22 1997 +0100 +++ b/src/HOL/MiniML/W.thy Tue Dec 30 11:14:09 1997 +0100 @@ -20,8 +20,8 @@ primrec W expr "W (Var i) A n = (if i < length A then Some( id_subst, - bound_typ_inst (%b. TVar(b+n)) (nth i A), - n + (min_new_bound_tv (nth i A)) ) + bound_typ_inst (%b. TVar(b+n)) (A!i), + n + (min_new_bound_tv (A!i)) ) else None)" "W (Abs e) A n = ( (S,t,m) := W e ((FVar n)#A) (Suc n);