src/Pure/term.ML
changeset 32020 9abf5d66606e
parent 30364 577edc39b501
child 32198 9bdd47909ea8
     1.1 --- a/src/Pure/term.ML	Thu Jul 16 20:32:40 2009 +0200
     1.2 +++ b/src/Pure/term.ML	Thu Jul 16 21:00:09 2009 +0200
     1.3 @@ -634,31 +634,31 @@
     1.4  *)
     1.5  fun subst_bounds (args: term list, t) : term =
     1.6    let
     1.7 -    exception SAME;
     1.8      val n = length args;
     1.9      fun subst (t as Bound i, lev) =
    1.10 -         (if i < lev then raise SAME   (*var is locally bound*)
    1.11 +         (if i < lev then raise Same.SAME   (*var is locally bound*)
    1.12            else incr_boundvars lev (nth args (i - lev))
    1.13              handle Subscript => Bound (i - n))  (*loose: change it*)
    1.14        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    1.15        | subst (f $ t, lev) =
    1.16 -          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    1.17 -      | subst _ = raise SAME;
    1.18 -  in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
    1.19 +          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
    1.20 +            handle Same.SAME => f $ subst (t, lev))
    1.21 +      | subst _ = raise Same.SAME;
    1.22 +  in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
    1.23  
    1.24  (*Special case: one argument*)
    1.25  fun subst_bound (arg, t) : term =
    1.26    let
    1.27 -    exception SAME;
    1.28      fun subst (Bound i, lev) =
    1.29 -          if i < lev then raise SAME   (*var is locally bound*)
    1.30 +          if i < lev then raise Same.SAME   (*var is locally bound*)
    1.31            else if i = lev then incr_boundvars lev arg
    1.32            else Bound (i - 1)   (*loose: change it*)
    1.33        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    1.34        | subst (f $ t, lev) =
    1.35 -          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    1.36 -      | subst _ = raise SAME;
    1.37 -  in subst (t, 0) handle SAME => t end;
    1.38 +          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
    1.39 +            handle Same.SAME => f $ subst (t, lev))
    1.40 +      | subst _ = raise Same.SAME;
    1.41 +  in subst (t, 0) handle Same.SAME => t end;
    1.42  
    1.43  (*beta-reduce if possible, else form application*)
    1.44  fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
    1.45 @@ -708,15 +708,16 @@
    1.46    The resulting term is ready to become the body of an Abs.*)
    1.47  fun abstract_over (v, body) =
    1.48    let
    1.49 -    exception SAME;
    1.50      fun abs lev tm =
    1.51        if v aconv tm then Bound lev
    1.52        else
    1.53          (case tm of
    1.54            Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
    1.55 -        | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
    1.56 -        | _ => raise SAME);
    1.57 -  in abs 0 body handle SAME => body end;
    1.58 +        | t $ u =>
    1.59 +            (abs lev t $ (abs lev u handle Same.SAME => u)
    1.60 +              handle Same.SAME => t $ abs lev u)
    1.61 +        | _ => raise Same.SAME);
    1.62 +  in abs 0 body handle Same.SAME => body end;
    1.63  
    1.64  fun lambda v t =
    1.65    let val x =