src/Pure/term.ML
changeset 18893 2dbf73278b0e
parent 18871 ca48320f6619
child 18927 2e5b0f3f1418
     1.1 --- a/src/Pure/term.ML	Thu Feb 02 12:52:16 2006 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Feb 02 12:52:18 2006 +0100
     1.3 @@ -194,8 +194,6 @@
     1.4    val maxidx_typs: typ list -> int -> int
     1.5    val maxidx_term: term -> int -> int
     1.6    val invent_names: string list -> string -> int -> string list
     1.7 -  val map_typ: (string -> string) -> (string -> string) -> typ -> typ
     1.8 -  val map_term: (string -> string) -> (string -> string) -> (string -> string) -> term -> term
     1.9    val dest_abs: string * typ * term -> string * term
    1.10    val bound: int -> string
    1.11    val is_bound: string -> bool
    1.12 @@ -1124,19 +1122,6 @@
    1.13  
    1.14  fun exists_Const P = exists_subterm (fn Const c => P c | _ => false);
    1.15  
    1.16 -(*map classes, tycons*)
    1.17 -fun map_typ f g (Type (c, Ts)) = Type (g c, map (map_typ f g) Ts)
    1.18 -  | map_typ f _ (TFree (x, S)) = TFree (x, map f S)
    1.19 -  | map_typ f _ (TVar (xi, S)) = TVar (xi, map f S);
    1.20 -
    1.21 -(*map classes, tycons, consts*)
    1.22 -fun map_term f g h (Const (c, T)) = Const (h c, map_typ f g T)
    1.23 -  | map_term f g _ (Free (x, T)) = Free (x, map_typ f g T)
    1.24 -  | map_term f g _ (Var (xi, T)) = Var (xi, map_typ f g T)
    1.25 -  | map_term _ _ _ (t as Bound _) = t
    1.26 -  | map_term f g h (Abs (x, T, t)) = Abs (x, map_typ f g T, map_term f g h t)
    1.27 -  | map_term f g h (t $ u) = map_term f g h t $ map_term f g h u;
    1.28 -
    1.29  
    1.30  (** TFrees and TVars **)
    1.31