1.1 --- a/src/Pure/term.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -311,7 +311,7 @@
     1.4  fun type_of1 (Ts, Const (_,T)) = T
     1.5    | type_of1 (Ts, Free  (_,T)) = T
     1.6    | type_of1 (Ts, Bound i) = (nth Ts i
     1.7 -        handle Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
     1.8 +        handle General.Subscript => raise TYPE("type_of: bound variable", [], [Bound i]))
     1.9    | type_of1 (Ts, Var (_,T)) = T
    1.10    | type_of1 (Ts, Abs (_,T,body)) = T --> type_of1(T::Ts, body)
    1.11    | type_of1 (Ts, f$u) =
    1.12 @@ -336,7 +336,7 @@
    1.13    | fastype_of1 (_, Const (_,T)) = T
    1.14    | fastype_of1 (_, Free (_,T)) = T
    1.15    | fastype_of1 (Ts, Bound i) = (nth Ts i
    1.16 -         handle Subscript => raise TERM("fastype_of: Bound", [Bound i]))
    1.17 +         handle General.Subscript => raise TERM("fastype_of: Bound", [Bound i]))
    1.18    | fastype_of1 (_, Var (_,T)) = T
    1.19    | fastype_of1 (Ts, Abs (_,T,u)) = T --> fastype_of1 (T::Ts, u);
    1.20  
    1.21 @@ -668,7 +668,7 @@
    1.22      fun subst (t as Bound i, lev) =
    1.23           (if i < lev then raise Same.SAME   (*var is locally bound*)
    1.24            else incr_boundvars lev (nth args (i - lev))
    1.25 -            handle Subscript => Bound (i - n))  (*loose: change it*)
    1.26 +            handle General.Subscript => Bound (i - n))  (*loose: change it*)
    1.27        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    1.28        | subst (f $ t, lev) =
    1.29            (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)