src/Pure/term.ML
changeset 15574 b1d1b5bfc464
parent 15573 cf53c2dcf440
child 15598 4ab52355bb53
     1.1 --- a/src/Pure/term.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/term.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -773,11 +773,11 @@
     1.4  
     1.5  (** Consts etc. **)
     1.6  
     1.7 -fun add_typ_classes (Type (_, Ts), cs) = Library.foldr add_typ_classes (Ts, cs)
     1.8 +fun add_typ_classes (Type (_, Ts), cs) = foldr add_typ_classes cs Ts
     1.9    | add_typ_classes (TFree (_, S), cs) = S union cs
    1.10    | add_typ_classes (TVar (_, S), cs) = S union cs;
    1.11  
    1.12 -fun add_typ_tycons (Type (c, Ts), cs) = Library.foldr add_typ_tycons (Ts, c ins cs)
    1.13 +fun add_typ_tycons (Type (c, Ts), cs) = foldr add_typ_tycons (c ins cs) Ts
    1.14    | add_typ_tycons (_, cs) = cs;
    1.15  
    1.16  val add_term_classes = it_term_types add_typ_classes;
    1.17 @@ -840,20 +840,20 @@
    1.18    | add_term_names (_, bs) = bs;
    1.19  
    1.20  (*Accumulates the TVars in a type, suppressing duplicates. *)
    1.21 -fun add_typ_tvars(Type(_,Ts),vs) = Library.foldr add_typ_tvars (Ts,vs)
    1.22 +fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
    1.23    | add_typ_tvars(TFree(_),vs) = vs
    1.24    | add_typ_tvars(TVar(v),vs) = v ins vs;
    1.25  
    1.26  (*Accumulates the TFrees in a type, suppressing duplicates. *)
    1.27 -fun add_typ_tfree_names(Type(_,Ts),fs) = Library.foldr add_typ_tfree_names (Ts,fs)
    1.28 +fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
    1.29    | add_typ_tfree_names(TFree(f,_),fs) = f ins_string fs
    1.30    | add_typ_tfree_names(TVar(_),fs) = fs;
    1.31  
    1.32 -fun add_typ_tfrees(Type(_,Ts),fs) = Library.foldr add_typ_tfrees (Ts,fs)
    1.33 +fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
    1.34    | add_typ_tfrees(TFree(f),fs) = f ins fs
    1.35    | add_typ_tfrees(TVar(_),fs) = fs;
    1.36  
    1.37 -fun add_typ_varnames(Type(_,Ts),nms) = Library.foldr add_typ_varnames (Ts,nms)
    1.38 +fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
    1.39    | add_typ_varnames(TFree(nm,_),nms) = nm ins_string nms
    1.40    | add_typ_varnames(TVar((nm,_),_),nms) = nm ins_string nms;
    1.41