src/Pure/sign.ML
changeset 30146 a77fc0209723
parent 29606 fedb8be05f24
child 30218 cdd82ba2b4fd
     1.1 --- a/src/Pure/sign.ML	Fri Feb 27 16:33:11 2009 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Feb 27 16:38:52 2009 +0100
     1.3 @@ -338,7 +338,7 @@
     1.4      fun typ_of (_, Const (_, T)) = T
     1.5        | typ_of (_, Free  (_, T)) = T
     1.6        | typ_of (_, Var (_, T)) = T
     1.7 -      | typ_of (bs, Bound i) = snd (List.nth (bs, i) handle Subscript =>
     1.8 +      | typ_of (bs, Bound i) = snd (nth bs i handle Subscript =>
     1.9            raise TYPE ("Loose bound variable: B." ^ string_of_int i, [], [Bound i]))
    1.10        | typ_of (bs, Abs (x, T, body)) = T --> typ_of ((x, T) :: bs, body)
    1.11        | typ_of (bs, t $ u) =