src/Pure/term.ML
changeset 20548 8ef25fe585a8
parent 20531 7de9caf4fd78
child 20664 ffbc5a57191a
     1.1 --- a/src/Pure/term.ML	Fri Sep 15 22:56:08 2006 +0200
     1.2 +++ b/src/Pure/term.ML	Fri Sep 15 22:56:13 2006 +0200
     1.3 @@ -68,7 +68,7 @@
     1.4    val map_aterms: (term -> term) -> term -> term
     1.5    val map_type_tvar: (indexname * sort -> typ) -> typ -> typ
     1.6    val map_type_tfree: (string * sort -> typ) -> typ -> typ
     1.7 -  val map_term_types: (typ -> typ) -> term -> term
     1.8 +  val map_types: (typ -> typ) -> term -> term
     1.9    val fold_atyps: (typ -> 'a -> 'a) -> typ -> 'a -> 'a
    1.10    val fold_aterms: (term -> 'a -> 'a) -> term -> 'a -> 'a
    1.11    val fold_term_types: (term -> typ -> 'a -> 'a) -> term -> 'a -> 'a
    1.12 @@ -423,7 +423,7 @@
    1.13  fun map_type_tvar f = map_atyps (fn TVar x => f x | T => T);
    1.14  fun map_type_tfree f = map_atyps (fn TFree x => f x | T => T);
    1.15  
    1.16 -fun map_term_types f =
    1.17 +fun map_types f =
    1.18    let
    1.19      fun map_aux (Const (a, T)) = Const (a, f T)
    1.20        | map_aux (Free (a, T)) = Free (a, f T)
    1.21 @@ -911,7 +911,7 @@
    1.22        in subst ty end;
    1.23  
    1.24  fun subst_atomic_types [] tm = tm
    1.25 -  | subst_atomic_types inst tm = map_term_types (typ_subst_atomic inst) tm;
    1.26 +  | subst_atomic_types inst tm = map_types (typ_subst_atomic inst) tm;
    1.27  
    1.28  fun typ_subst_TVars [] ty = ty
    1.29    | typ_subst_TVars inst ty =
    1.30 @@ -922,7 +922,7 @@
    1.31        in subst ty end;
    1.32  
    1.33  fun subst_TVars [] tm = tm
    1.34 -  | subst_TVars inst tm = map_term_types (typ_subst_TVars inst) tm;
    1.35 +  | subst_TVars inst tm = map_types (typ_subst_TVars inst) tm;
    1.36  
    1.37  fun subst_Vars [] tm = tm
    1.38    | subst_Vars inst tm =