| changeset 18976 | 4efb82669880 |
| parent 18975 | 78d650a7e99a |
| child 18981 | a7b7cf408cff |
--- 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)