src/Pure/envir.ML
changeset 15570 8d8c70b41bab
parent 15531 08c8dad8e399
child 15797 a63605582573
     1.1 --- a/src/Pure/envir.ML	Thu Mar 03 09:22:35 2005 +0100
     1.2 +++ b/src/Pure/envir.ML	Thu Mar 03 12:43:01 2005 +0100
     1.3 @@ -197,8 +197,8 @@
     1.4        | fast Ts (Const (_, T)) = T
     1.5        | fast Ts (Free (_, T)) = T
     1.6        | fast Ts (Bound i) =
     1.7 -	(nth_elem (i, Ts)
     1.8 -  	 handle LIST _=> raise TERM ("fastype: Bound", [Bound i]))
     1.9 +	(List.nth (Ts, i)
    1.10 +  	 handle Subscript => raise TERM ("fastype: Bound", [Bound i]))
    1.11        | fast Ts (Var (_, T)) = T 
    1.12        | fast Ts (Abs (_, T, u)) = T --> fast (T :: Ts) u
    1.13  in fast end;