1.1 --- a/src/Pure/logic.ML	Thu Jul 16 20:32:40 2009 +0200
     1.2 +++ b/src/Pure/logic.ML	Thu Jul 16 21:00:09 2009 +0200
     1.3 @@ -304,44 +304,33 @@
     1.4    | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
     1.5  
     1.6  
     1.7 -local exception SAME in
     1.8 -
     1.9 -fun incrT k =
    1.10 -  let
    1.11 -    fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
    1.12 -      | incr (Type (a, Ts)) = Type (a, incrs Ts)
    1.13 -      | incr _ = raise SAME
    1.14 -    and incrs (T :: Ts) =
    1.15 -        (incr T :: (incrs Ts handle SAME => Ts)
    1.16 -          handle SAME => T :: incrs Ts)
    1.17 -      | incrs [] = raise SAME;
    1.18 -  in incr end;
    1.19 +fun incrT k = Term_Subst.map_atypsT_same
    1.20 +  (fn TVar ((a, i), S) => TVar ((a, i + k), S)
    1.21 +    | _ => raise Same.SAME);
    1.22  
    1.23  (*For all variables in the term, increment indexnames and lift over the Us
    1.24      result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
    1.25  fun incr_indexes ([], 0) t = t
    1.26    | incr_indexes (Ts, k) t =
    1.27 -  let
    1.28 -    val n = length Ts;
    1.29 -    val incrT = if k = 0 then I else incrT k;
    1.30 +      let
    1.31 +        val n = length Ts;
    1.32 +        val incrT = if k = 0 then I else incrT k;
    1.33  
    1.34 -    fun incr lev (Var ((x, i), T)) =
    1.35 -          combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
    1.36 -      | incr lev (Abs (x, T, body)) =
    1.37 -          (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
    1.38 -            handle SAME => Abs (x, T, incr (lev + 1) body))
    1.39 -      | incr lev (t $ u) =
    1.40 -          (incr lev t $ (incr lev u handle SAME => u)
    1.41 -            handle SAME => t $ incr lev u)
    1.42 -      | incr _ (Const (c, T)) = Const (c, incrT T)
    1.43 -      | incr _ (Free (x, T)) = Free (x, incrT T)
    1.44 -      | incr _ (t as Bound _) = t;
    1.45 -  in incr 0 t handle SAME => t end;
    1.46 +        fun incr lev (Var ((x, i), T)) =
    1.47 +              combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
    1.48 +          | incr lev (Abs (x, T, body)) =
    1.49 +              (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
    1.50 +                handle Same.SAME => Abs (x, T, incr (lev + 1) body))
    1.51 +          | incr lev (t $ u) =
    1.52 +              (incr lev t $ (incr lev u handle Same.SAME => u)
    1.53 +                handle Same.SAME => t $ incr lev u)
    1.54 +          | incr _ (Const (c, T)) = Const (c, incrT T)
    1.55 +          | incr _ (Free (x, T)) = Free (x, incrT T)
    1.56 +          | incr _ (t as Bound _) = t;
    1.57 +      in incr 0 t handle Same.SAME => t end;
    1.58  
    1.59  fun incr_tvar 0 T = T
    1.60 -  | incr_tvar k T = incrT k T handle SAME => T;
    1.61 -
    1.62 -end;
    1.63 +  | incr_tvar k T = incrT k T handle Same.SAME => T;
    1.64  
    1.65  
    1.66  (* Lifting functions from subgoal and increment:
    1.67 @@ -473,35 +462,35 @@
    1.68  fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
    1.69  fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
    1.70  
    1.71 -fun varifyT_option ty = ty
    1.72 -  |> Term_Subst.map_atypsT_option
    1.73 -    (fn TFree (a, S) => SOME (TVar ((a, 0), S))
    1.74 +fun varifyT_same ty = ty
    1.75 +  |> Term_Subst.map_atypsT_same
    1.76 +    (fn TFree (a, S) => TVar ((a, 0), S)
    1.77        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
    1.78  
    1.79 -fun unvarifyT_option ty = ty
    1.80 -  |> Term_Subst.map_atypsT_option
    1.81 -    (fn TVar ((a, 0), S) => SOME (TFree (a, S))
    1.82 +fun unvarifyT_same ty = ty
    1.83 +  |> Term_Subst.map_atypsT_same
    1.84 +    (fn TVar ((a, 0), S) => TFree (a, S)
    1.85        | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
    1.86        | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
    1.87  
    1.88 -val varifyT = perhaps varifyT_option;
    1.89 -val unvarifyT = perhaps unvarifyT_option;
    1.90 +val varifyT = Same.commit varifyT_same;
    1.91 +val unvarifyT = Same.commit unvarifyT_same;
    1.92  
    1.93  fun varify tm = tm
    1.94 -  |> perhaps (Term_Subst.map_aterms_option
    1.95 -    (fn Free (x, T) => SOME (Var ((x, 0), T))
    1.96 +  |> Same.commit (Term_Subst.map_aterms_same
    1.97 +    (fn Free (x, T) => Var ((x, 0), T)
    1.98        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
    1.99 -      | _ => NONE))
   1.100 -  |> perhaps (Term_Subst.map_types_option varifyT_option)
   1.101 +      | _ => raise Same.SAME))
   1.102 +  |> Same.commit (Term_Subst.map_types_same varifyT_same)
   1.103    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   1.104  
   1.105  fun unvarify tm = tm
   1.106 -  |> perhaps (Term_Subst.map_aterms_option
   1.107 -    (fn Var ((x, 0), T) => SOME (Free (x, T))
   1.108 +  |> Same.commit (Term_Subst.map_aterms_same
   1.109 +    (fn Var ((x, 0), T) => Free (x, T)
   1.110        | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
   1.111        | Free (x, _) => raise TERM (bad_fixed x, [tm])
   1.112 -      | _ => NONE))
   1.113 -  |> perhaps (Term_Subst.map_types_option unvarifyT_option)
   1.114 +      | _ => raise Same.SAME))
   1.115 +  |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
   1.116    handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
   1.117  
   1.118  

     2.1 --- a/src/Pure/term.ML	Thu Jul 16 20:32:40 2009 +0200
     2.2 +++ b/src/Pure/term.ML	Thu Jul 16 21:00:09 2009 +0200
     2.3 @@ -634,31 +634,31 @@
     2.4  *)
     2.5  fun subst_bounds (args: term list, t) : term =
     2.6    let
     2.7 -    exception SAME;
     2.8      val n = length args;
     2.9      fun subst (t as Bound i, lev) =
    2.10 -         (if i < lev then raise SAME   (*var is locally bound*)
    2.11 +         (if i < lev then raise Same.SAME   (*var is locally bound*)
    2.12            else incr_boundvars lev (nth args (i - lev))
    2.13              handle Subscript => Bound (i - n))  (*loose: change it*)
    2.14        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    2.15        | subst (f $ t, lev) =
    2.16 -          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    2.17 -      | subst _ = raise SAME;
    2.18 -  in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
    2.19 +          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
    2.20 +            handle Same.SAME => f $ subst (t, lev))
    2.21 +      | subst _ = raise Same.SAME;
    2.22 +  in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
    2.23  
    2.24  (*Special case: one argument*)
    2.25  fun subst_bound (arg, t) : term =
    2.26    let
    2.27 -    exception SAME;
    2.28      fun subst (Bound i, lev) =
    2.29 -          if i < lev then raise SAME   (*var is locally bound*)
    2.30 +          if i < lev then raise Same.SAME   (*var is locally bound*)
    2.31            else if i = lev then incr_boundvars lev arg
    2.32            else Bound (i - 1)   (*loose: change it*)
    2.33        | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
    2.34        | subst (f $ t, lev) =
    2.35 -          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
    2.36 -      | subst _ = raise SAME;
    2.37 -  in subst (t, 0) handle SAME => t end;
    2.38 +          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
    2.39 +            handle Same.SAME => f $ subst (t, lev))
    2.40 +      | subst _ = raise Same.SAME;
    2.41 +  in subst (t, 0) handle Same.SAME => t end;
    2.42  
    2.43  (*beta-reduce if possible, else form application*)
    2.44  fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
    2.45 @@ -708,15 +708,16 @@
    2.46    The resulting term is ready to become the body of an Abs.*)
    2.47  fun abstract_over (v, body) =
    2.48    let
    2.49 -    exception SAME;
    2.50      fun abs lev tm =
    2.51        if v aconv tm then Bound lev
    2.52        else
    2.53          (case tm of
    2.54            Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
    2.55 -        | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
    2.56 -        | _ => raise SAME);
    2.57 -  in abs 0 body handle SAME => body end;
    2.58 +        | t $ u =>
    2.59 +            (abs lev t $ (abs lev u handle Same.SAME => u)
    2.60 +              handle Same.SAME => t $ abs lev u)
    2.61 +        | _ => raise Same.SAME);
    2.62 +  in abs 0 body handle Same.SAME => body end;
    2.63  
    2.64  fun lambda v t =
    2.65    let val x =

     3.1 --- a/src/Pure/term_subst.ML	Thu Jul 16 20:32:40 2009 +0200
     3.2 +++ b/src/Pure/term_subst.ML	Thu Jul 16 21:00:09 2009 +0200
     3.3 @@ -39,10 +39,8 @@
     3.4  
     3.5  fun map_atypsT_same f =
     3.6    let
     3.7 -    fun typ (Type (a, Ts)) = Type (a, typs Ts)
     3.8 -      | typ T = f T
     3.9 -    and typs (T :: Ts) = (typ T :: Same.commit typs Ts handle Same.SAME => T :: typs Ts)
    3.10 -      | typs [] = raise Same.SAME;
    3.11 +    fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
    3.12 +      | typ T = f T;
    3.13    in typ end;
    3.14  
    3.15  fun map_types_same f =
    3.16 @@ -50,7 +48,7 @@
    3.17      fun term (Const (a, T)) = Const (a, f T)
    3.18        | term (Free (a, T)) = Free (a, f T)
    3.19        | term (Var (v, T)) = Var (v, f T)
    3.20 -      | term (Bound _)  = raise Same.SAME
    3.21 +      | term (Bound _) = raise Same.SAME
    3.22        | term (Abs (x, T, t)) =
    3.23            (Abs (x, f T, Same.commit term t)
    3.24              handle Same.SAME => Abs (x, T, term t))
    3.25 @@ -77,16 +75,12 @@
    3.26  fun generalizeT_same [] _ _ = raise Same.SAME
    3.27    | generalizeT_same tfrees idx ty =
    3.28        let
    3.29 -        fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
    3.30 -          | gen_typ (TFree (a, S)) =
    3.31 +        fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
    3.32 +          | gen (TFree (a, S)) =
    3.33                if member (op =) tfrees a then TVar ((a, idx), S)
    3.34                else raise Same.SAME
    3.35 -          | gen_typ _ = raise Same.SAME
    3.36 -        and gen_typs (T :: Ts) =
    3.37 -            (gen_typ T :: Same.commit gen_typs Ts
    3.38 -              handle Same.SAME => T :: gen_typs Ts)
    3.39 -          | gen_typs [] = raise Same.SAME;
    3.40 -      in gen_typ ty end;
    3.41 +          | gen _ = raise Same.SAME;
    3.42 +      in gen ty end;
    3.43  
    3.44  fun generalize_same ([], []) _ _ = raise Same.SAME
    3.45    | generalize_same (tfrees, frees) idx tm =