src/Pure/sign.ML
changeset 18892 51360da418b2
parent 18857 c4b4fbd74ffb
child 18928 042608ffa2ec
     1.1 --- a/src/Pure/sign.ML	Thu Feb 02 10:24:06 2006 +0100
     1.2 +++ b/src/Pure/sign.ML	Thu Feb 02 12:52:16 2006 +0100
     1.3 @@ -309,6 +309,17 @@
     1.4  
     1.5  local
     1.6  
     1.7 +fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
     1.8 +  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
     1.9 +  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.10 +
    1.11 +fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.12 +  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.13 +  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.14 +  | map_term _ _ _ (t as Bound _) = t
    1.15 +  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.16 +  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.17 +
    1.18  fun mapping add_names f t =
    1.19    let
    1.20      fun f' x = let val y = f x in if x = y then NONE else SOME (x, y) end;
    1.21 @@ -317,12 +328,12 @@
    1.22    in get end;
    1.23  
    1.24  fun typ_mapping f g thy T =
    1.25 -  T |> Term.map_typ
    1.26 +  T |> map_typ
    1.27      (mapping add_typ_classes (f thy) T)
    1.28      (mapping add_typ_tycons (g thy) T);
    1.29  
    1.30  fun term_mapping f g h thy t =
    1.31 -  t |> Term.map_term
    1.32 +  t |> map_term
    1.33      (mapping add_term_classes (f thy) t)
    1.34      (mapping add_term_tycons (g thy) t)
    1.35      (mapping add_term_consts (h thy) t);