# HG changeset patch
# User berghofe
# Date 952696924 -3600
# Node ID 5902c02fa1227a081116016c00e1a5c018a99286
# Parent  ef01ee11b14ea8757a937a2efeca60a87cb39334
Type.unify now uses Vartab instead of association lists.

diff -r ef01ee11b14e -r 5902c02fa122 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Fri Mar 10 15:00:32 2000 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Fri Mar 10 15:02:04 2000 +0100
@@ -188,8 +188,8 @@
       in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
           (env, (replicate (length consts) cT) ~~ consts)
       end;
-    val (env, _) = foldl unify (([], i'), rec_consts);
-    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars env T
+    val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);
+    fun typ_subst_TVars_2 env T = let val T' = typ_subst_TVars_Vartab env T
       in if T = T' then T else typ_subst_TVars_2 env T' end;
     val subst = fst o Type.freeze_thaw o
       (map_term_types (typ_subst_TVars_2 env))