author | haftmann |
Wed, 08 Feb 2006 09:27:20 +0100 | |
changeset 18976 | 4efb82669880 |
parent 18975 | 78d650a7e99a |
child 18977 | f24c416a4814 |
src/Pure/term.ML | file | annotate | diff | comparison | revisions |
--- a/src/Pure/term.ML Tue Feb 07 19:57:00 2006 +0100 +++ b/src/Pure/term.ML Wed Feb 08 09:27:20 2006 +0100 @@ -442,7 +442,7 @@ in add_size (tm, 0) end; fun map_atyps f (Type (a, Ts)) = Type (a, map (map_atyps f) Ts) - | map_atyps f T = T; + | map_atyps f T = f T; fun map_aterms f (t $ u) = map_aterms f t $ map_aterms f u | map_aterms f (Abs (a, T, t)) = Abs (a, T, map_aterms f t)