diff -r fd6b42e6bf50 -r a7b7cf408cff src/Pure/term.ML
--- a/src/Pure/term.ML	Wed Feb 08 17:15:27 2006 +0100
+++ b/src/Pure/term.ML	Wed Feb 08 17:15:28 2006 +0100
@@ -448,19 +448,8 @@
   | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
   | map_aterms f t = f t;
 
-fun map_type_tvar f =
-  let
-    fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
-      | map_aux (TVar x) = f x
-      | map_aux T = T;
-  in map_aux end;
-
-fun map_type_tfree f =
-  let
-    fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
-      | map_aux (TFree x) = f x
-      | map_aux T = T;
-  in map_aux end;
+fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
+fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
 
 fun map_term_types f =
   let