Type.unify now uses Vartab instead of association lists.
authorberghofe
Fri Mar 10 15:02:04 2000 +0100 (2000-03-10)
changeset 84105902c02fa122
parent 8409 ef01ee11b14e
child 8411 d30df828a974
Type.unify now uses Vartab instead of association lists.
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Fri Mar 10 15:00:32 2000 +0100
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 10 15:02:04 2000 +0100
     1.3 @@ -188,8 +188,8 @@
     1.4        in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
     1.5            (env, (replicate (length consts) cT) ~~ consts)
     1.6        end;
     1.7 -    val (env, _) = foldl unify (([], i'), rec_consts);
     1.8 -    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
     1.9 +    val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
    1.10 +    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
    1.11        in if T = T' then T else typ_subst_TVars_2 env T' end;
    1.12      val subst = fst o Type.freeze_thaw o
    1.13        (map_term_types (typ_subst_TVars_2 env))