1.1 --- a/src/Pure/term.ML	Thu May 31 23:02:16 2007 +0200
     1.2 +++ b/src/Pure/term.ML	Thu May 31 23:47:36 2007 +0200
     1.3 @@ -1112,20 +1112,20 @@
     1.4    | add_term_names (_, bs) = bs;
     1.5  
     1.6  (*Accumulates the TVars in a type, suppressing duplicates. *)
     1.7 -fun add_typ_tvars(Type(_,Ts),vs) = foldr add_typ_tvars vs Ts
     1.8 +fun add_typ_tvars(Type(_,Ts),vs) = List.foldr add_typ_tvars vs Ts
     1.9    | add_typ_tvars(TFree(_),vs) = vs
    1.10    | add_typ_tvars(TVar(v),vs) = insert (op =) v vs;
    1.11  
    1.12  (*Accumulates the TFrees in a type, suppressing duplicates. *)
    1.13 -fun add_typ_tfree_names(Type(_,Ts),fs) = foldr add_typ_tfree_names fs Ts
    1.14 +fun add_typ_tfree_names(Type(_,Ts),fs) = List.foldr add_typ_tfree_names fs Ts
    1.15    | add_typ_tfree_names(TFree(f,_),fs) = insert (op =) f fs
    1.16    | add_typ_tfree_names(TVar(_),fs) = fs;
    1.17  
    1.18 -fun add_typ_tfrees(Type(_,Ts),fs) = foldr add_typ_tfrees fs Ts
    1.19 +fun add_typ_tfrees(Type(_,Ts),fs) = List.foldr add_typ_tfrees fs Ts
    1.20    | add_typ_tfrees(TFree(f),fs) = insert (op =) f fs
    1.21    | add_typ_tfrees(TVar(_),fs) = fs;
    1.22  
    1.23 -fun add_typ_varnames(Type(_,Ts),nms) = foldr add_typ_varnames nms Ts
    1.24 +fun add_typ_varnames(Type(_,Ts),nms) = List.foldr add_typ_varnames nms Ts
    1.25    | add_typ_varnames(TFree(nm,_),nms) = insert (op =) nm nms
    1.26    | add_typ_varnames(TVar((nm,_),_),nms) = insert (op =) nm nms;
    1.27