src/Pure/proofterm.ML
changeset 43278 1fbdcebb364b
parent 41699 21492e1c2b5a
child 43324 2b47822868e4
     1.1 --- a/src/Pure/proofterm.ML	Wed Jun 08 15:39:55 2011 +0200
     1.2 +++ b/src/Pure/proofterm.ML	Wed Jun 08 15:56:57 2011 +0200
     1.3 @@ -529,7 +529,7 @@
     1.4      fun subst' lev (Bound i) =
     1.5           (if i<lev then raise Same.SAME    (*var is locally bound*)
     1.6            else  incr_boundvars lev (nth args (i-lev))
     1.7 -                  handle Subscript => Bound (i-n))  (*loose: change it*)
     1.8 +                  handle General.Subscript => Bound (i-n))  (*loose: change it*)
     1.9        | subst' lev (Abs (a, T, body)) = Abs (a, T,  subst' (lev+1) body)
    1.10        | subst' lev (f $ t) = (subst' lev f $ substh' lev t
    1.11            handle Same.SAME => f $ subst' lev t)
    1.12 @@ -554,7 +554,7 @@
    1.13      fun subst (PBound i) Plev tlev =
    1.14           (if i < Plev then raise Same.SAME    (*var is locally bound*)
    1.15            else incr_pboundvars Plev tlev (nth args (i-Plev))
    1.16 -                 handle Subscript => PBound (i-n)  (*loose: change it*))
    1.17 +                 handle General.Subscript => PBound (i-n)  (*loose: change it*))
    1.18        | subst (AbsP (a, t, body)) Plev tlev = AbsP (a, t, subst body (Plev+1) tlev)
    1.19        | subst (Abst (a, T, body)) Plev tlev = Abst (a, T, subst body Plev (tlev+1))
    1.20        | subst (prf %% prf') Plev tlev = (subst prf Plev tlev %% substh prf' Plev tlev