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 =