src/Pure/type.ML
changeset 15574 b1d1b5bfc464
parent 15570 8d8c70b41bab
child 15797 a63605582573
     1.1 --- a/src/Pure/type.ML	Fri Mar 04 11:44:26 2005 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Mar 04 15:07:34 2005 +0100
     1.3 @@ -252,14 +252,14 @@
     1.4    let
     1.5      val used = add_typ_tfree_names (T, [])
     1.6      and tvars = map #1 (add_typ_tvars (T, []));
     1.7 -    val (alist, _) = Library.foldr new_name (tvars, ([], used));
     1.8 +    val (alist, _) = foldr new_name ([], used) tvars;
     1.9    in (map_type_tvar (freeze_one alist) T, map_type_tfree (thaw_one (map swap alist))) end;
    1.10  
    1.11  fun freeze_thaw t =
    1.12    let
    1.13      val used = it_term_types add_typ_tfree_names (t, [])
    1.14      and tvars = map #1 (it_term_types add_typ_tvars (t, []));
    1.15 -    val (alist, _) = Library.foldr new_name (tvars, ([], used));
    1.16 +    val (alist, _) = foldr new_name ([], used) tvars;
    1.17    in
    1.18      (case alist of
    1.19        [] => (t, fn x => x) (*nothing to do!*)
    1.20 @@ -378,7 +378,7 @@
    1.21            else meet ((T, S), Vartab.update_new ((v, T), tye))
    1.22        | (Type (a, Ts), Type (b, Us)) =>
    1.23            if a <> b then raise TUNIFY
    1.24 -          else Library.foldr unif (Ts ~~ Us, tye)
    1.25 +          else foldr unif tye (Ts ~~ Us)
    1.26        | (T, U) => if T = U then tye else raise TUNIFY);
    1.27    in (unif (TU, tyenv), ! tyvar_count) end;
    1.28