src/Pure/term.ML
changeset 18981 a7b7cf408cff
parent 18976 4efb82669880
child 18995 ff4e4773cc7c
     1.1 --- a/src/Pure/term.ML	Wed Feb 08 17:15:27 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Wed Feb 08 17:15:28 2006 +0100
     1.3 @@ -448,19 +448,8 @@
     1.4    | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)
     1.5    | map_aterms f t = f t;
     1.6  
     1.7 -fun map_type_tvar f =
     1.8 -  let
     1.9 -    fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
    1.10 -      | map_aux (TVar x) = f x
    1.11 -      | map_aux T = T;
    1.12 -  in map_aux end;
    1.13 -
    1.14 -fun map_type_tfree f =
    1.15 -  let
    1.16 -    fun map_aux (Type (a, Ts)) = Type (a, map map_aux Ts)
    1.17 -      | map_aux (TFree x) = f x
    1.18 -      | map_aux T = T;
    1.19 -  in map_aux end;
    1.20 +fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
    1.21 +fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
    1.22  
    1.23  fun map_term_types f =
    1.24    let