# HG changeset patch
# User wenzelm
# Date 1247770809 -7200
# Node ID 9abf5d66606e6ece4850f8b7c8d09b502c327c64
# Parent  827a8ebb3b2cc7cbd717b1d67ae31c34a329a4c1
use structure Same;
tuned;

diff -r 827a8ebb3b2c -r 9abf5d66606e src/Pure/logic.ML
--- a/src/Pure/logic.ML	Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/logic.ML	Thu Jul 16 21:00:09 2009 +0200
@@ -304,44 +304,33 @@
   | rlist_abs ((a,T)::pairs, body) = rlist_abs(pairs, Abs(a, T, body));
 
 
-local exception SAME in
-
-fun incrT k =
-  let
-    fun incr (TVar ((a, i), S)) = TVar ((a, i + k), S)
-      | incr (Type (a, Ts)) = Type (a, incrs Ts)
-      | incr _ = raise SAME
-    and incrs (T :: Ts) =
-        (incr T :: (incrs Ts handle SAME => Ts)
-          handle SAME => T :: incrs Ts)
-      | incrs [] = raise SAME;
-  in incr end;
+fun incrT k = Term_Subst.map_atypsT_same
+  (fn TVar ((a, i), S) => TVar ((a, i + k), S)
+    | _ => raise Same.SAME);
 
 (*For all variables in the term, increment indexnames and lift over the Us
     result is ?Gidx(B.(lev+n-1),...,B.lev) where lev is abstraction level *)
 fun incr_indexes ([], 0) t = t
   | incr_indexes (Ts, k) t =
-  let
-    val n = length Ts;
-    val incrT = if k = 0 then I else incrT k;
+      let
+        val n = length Ts;
+        val incrT = if k = 0 then I else incrT k;
 
-    fun incr lev (Var ((x, i), T)) =
-          combound (Var ((x, i + k), Ts ---> (incrT T handle SAME => T)), lev, n)
-      | incr lev (Abs (x, T, body)) =
-          (Abs (x, incrT T, incr (lev + 1) body handle SAME => body)
-            handle SAME => Abs (x, T, incr (lev + 1) body))
-      | incr lev (t $ u) =
-          (incr lev t $ (incr lev u handle SAME => u)
-            handle SAME => t $ incr lev u)
-      | incr _ (Const (c, T)) = Const (c, incrT T)
-      | incr _ (Free (x, T)) = Free (x, incrT T)
-      | incr _ (t as Bound _) = t;
-  in incr 0 t handle SAME => t end;
+        fun incr lev (Var ((x, i), T)) =
+              combound (Var ((x, i + k), Ts ---> Same.commit incrT T), lev, n)
+          | incr lev (Abs (x, T, body)) =
+              (Abs (x, incrT T, incr (lev + 1) body handle Same.SAME => body)
+                handle Same.SAME => Abs (x, T, incr (lev + 1) body))
+          | incr lev (t $ u) =
+              (incr lev t $ (incr lev u handle Same.SAME => u)
+                handle Same.SAME => t $ incr lev u)
+          | incr _ (Const (c, T)) = Const (c, incrT T)
+          | incr _ (Free (x, T)) = Free (x, incrT T)
+          | incr _ (t as Bound _) = t;
+      in incr 0 t handle Same.SAME => t end;
 
 fun incr_tvar 0 T = T
-  | incr_tvar k T = incrT k T handle SAME => T;
-
-end;
+  | incr_tvar k T = incrT k T handle Same.SAME => T;
 
 
 (* Lifting functions from subgoal and increment:
@@ -473,35 +462,35 @@
 fun bad_schematic xi = "Illegal schematic variable: " ^ quote (Term.string_of_vname xi);
 fun bad_fixed x = "Illegal fixed variable: " ^ quote x;
 
-fun varifyT_option ty = ty
-  |> Term_Subst.map_atypsT_option
-    (fn TFree (a, S) => SOME (TVar ((a, 0), S))
+fun varifyT_same ty = ty
+  |> Term_Subst.map_atypsT_same
+    (fn TFree (a, S) => TVar ((a, 0), S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], []));
 
-fun unvarifyT_option ty = ty
-  |> Term_Subst.map_atypsT_option
-    (fn TVar ((a, 0), S) => SOME (TFree (a, S))
+fun unvarifyT_same ty = ty
+  |> Term_Subst.map_atypsT_same
+    (fn TVar ((a, 0), S) => TFree (a, S)
       | TVar (ai, _) => raise TYPE (bad_schematic ai, [ty], [])
       | TFree (a, _) => raise TYPE (bad_fixed a, [ty], []));
 
-val varifyT = perhaps varifyT_option;
-val unvarifyT = perhaps unvarifyT_option;
+val varifyT = Same.commit varifyT_same;
+val unvarifyT = Same.commit unvarifyT_same;
 
 fun varify tm = tm
-  |> perhaps (Term_Subst.map_aterms_option
-    (fn Free (x, T) => SOME (Var ((x, 0), T))
+  |> Same.commit (Term_Subst.map_aterms_same
+    (fn Free (x, T) => Var ((x, 0), T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
-      | _ => NONE))
-  |> perhaps (Term_Subst.map_types_option varifyT_option)
+      | _ => raise Same.SAME))
+  |> Same.commit (Term_Subst.map_types_same varifyT_same)
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 fun unvarify tm = tm
-  |> perhaps (Term_Subst.map_aterms_option
-    (fn Var ((x, 0), T) => SOME (Free (x, T))
+  |> Same.commit (Term_Subst.map_aterms_same
+    (fn Var ((x, 0), T) => Free (x, T)
       | Var (xi, _) => raise TERM (bad_schematic xi, [tm])
       | Free (x, _) => raise TERM (bad_fixed x, [tm])
-      | _ => NONE))
-  |> perhaps (Term_Subst.map_types_option unvarifyT_option)
+      | _ => raise Same.SAME))
+  |> Same.commit (Term_Subst.map_types_same unvarifyT_same)
   handle TYPE (msg, _, _) => raise TERM (msg, [tm]);
 
 
diff -r 827a8ebb3b2c -r 9abf5d66606e src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/term.ML	Thu Jul 16 21:00:09 2009 +0200
@@ -634,31 +634,31 @@
 *)
 fun subst_bounds (args: term list, t) : term =
   let
-    exception SAME;
     val n = length args;
     fun subst (t as Bound i, lev) =
-         (if i < lev then raise SAME   (*var is locally bound*)
+         (if i < lev then raise Same.SAME   (*var is locally bound*)
           else incr_boundvars lev (nth args (i - lev))
             handle Subscript => Bound (i - n))  (*loose: change it*)
       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
       | subst (f $ t, lev) =
-          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
-      | subst _ = raise SAME;
-  in case args of [] => t | _ => (subst (t, 0) handle SAME => t) end;
+          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+            handle Same.SAME => f $ subst (t, lev))
+      | subst _ = raise Same.SAME;
+  in case args of [] => t | _ => (subst (t, 0) handle Same.SAME => t) end;
 
 (*Special case: one argument*)
 fun subst_bound (arg, t) : term =
   let
-    exception SAME;
     fun subst (Bound i, lev) =
-          if i < lev then raise SAME   (*var is locally bound*)
+          if i < lev then raise Same.SAME   (*var is locally bound*)
           else if i = lev then incr_boundvars lev arg
           else Bound (i - 1)   (*loose: change it*)
       | subst (Abs (a, T, body), lev) = Abs (a, T, subst (body, lev + 1))
       | subst (f $ t, lev) =
-          (subst (f, lev) $ (subst (t, lev) handle SAME => t) handle SAME => f $ subst (t, lev))
-      | subst _ = raise SAME;
-  in subst (t, 0) handle SAME => t end;
+          (subst (f, lev) $ (subst (t, lev) handle Same.SAME => t)
+            handle Same.SAME => f $ subst (t, lev))
+      | subst _ = raise Same.SAME;
+  in subst (t, 0) handle Same.SAME => t end;
 
 (*beta-reduce if possible, else form application*)
 fun betapply (Abs(_,_,t), u) = subst_bound (u,t)
@@ -708,15 +708,16 @@
   The resulting term is ready to become the body of an Abs.*)
 fun abstract_over (v, body) =
   let
-    exception SAME;
     fun abs lev tm =
       if v aconv tm then Bound lev
       else
         (case tm of
           Abs (a, T, t) => Abs (a, T, abs (lev + 1) t)
-        | t $ u => (abs lev t $ (abs lev u handle SAME => u) handle SAME => t $ abs lev u)
-        | _ => raise SAME);
-  in abs 0 body handle SAME => body end;
+        | t $ u =>
+            (abs lev t $ (abs lev u handle Same.SAME => u)
+              handle Same.SAME => t $ abs lev u)
+        | _ => raise Same.SAME);
+  in abs 0 body handle Same.SAME => body end;
 
 fun lambda v t =
   let val x =
diff -r 827a8ebb3b2c -r 9abf5d66606e src/Pure/term_subst.ML
--- a/src/Pure/term_subst.ML	Thu Jul 16 20:32:40 2009 +0200
+++ b/src/Pure/term_subst.ML	Thu Jul 16 21:00:09 2009 +0200
@@ -39,10 +39,8 @@
 
 fun map_atypsT_same f =
   let
-    fun typ (Type (a, Ts)) = Type (a, typs Ts)
-      | typ T = f T
-    and typs (T :: Ts) = (typ T :: Same.commit typs Ts handle Same.SAME => T :: typs Ts)
-      | typs [] = raise Same.SAME;
+    fun typ (Type (a, Ts)) = Type (a, Same.map typ Ts)
+      | typ T = f T;
   in typ end;
 
 fun map_types_same f =
@@ -50,7 +48,7 @@
     fun term (Const (a, T)) = Const (a, f T)
       | term (Free (a, T)) = Free (a, f T)
       | term (Var (v, T)) = Var (v, f T)
-      | term (Bound _)  = raise Same.SAME
+      | term (Bound _) = raise Same.SAME
       | term (Abs (x, T, t)) =
           (Abs (x, f T, Same.commit term t)
             handle Same.SAME => Abs (x, T, term t))
@@ -77,16 +75,12 @@
 fun generalizeT_same [] _ _ = raise Same.SAME
   | generalizeT_same tfrees idx ty =
       let
-        fun gen_typ (Type (a, Ts)) = Type (a, gen_typs Ts)
-          | gen_typ (TFree (a, S)) =
+        fun gen (Type (a, Ts)) = Type (a, Same.map gen Ts)
+          | gen (TFree (a, S)) =
               if member (op =) tfrees a then TVar ((a, idx), S)
               else raise Same.SAME
-          | gen_typ _ = raise Same.SAME
-        and gen_typs (T :: Ts) =
-            (gen_typ T :: Same.commit gen_typs Ts
-              handle Same.SAME => T :: gen_typs Ts)
-          | gen_typs [] = raise Same.SAME;
-      in gen_typ ty end;
+          | gen _ = raise Same.SAME;
+      in gen ty end;
 
 fun generalize_same ([], []) _ _ = raise Same.SAME
   | generalize_same (tfrees, frees) idx tm =