src/HOL/Tools/inductive_package.ML
changeset 12527 d6c91bc3e49c
parent 12494 58848edad3c4
child 12609 fb073a34b537
--- a/src/HOL/Tools/inductive_package.ML	Mon Dec 17 14:27:18 2001 +0100
+++ b/src/HOL/Tools/inductive_package.ML	Tue Dec 18 02:17:20 2001 +0100
@@ -190,7 +190,7 @@
     val intr_consts = foldl add_term_consts_2 ([], intr_ts');
     fun unify (env, (cname, cT)) =
       let val consts = map snd (filter (fn c => fst c = cname) intr_consts)
-      in foldl (fn ((env', j'), Tp) => (Type.unify tsig j' env' Tp))
+      in foldl (fn ((env', j'), Tp) => (Type.unify tsig (env', j') Tp))
           (env, (replicate (length consts) cT) ~~ consts)
       end;
     val (env, _) = foldl unify ((Vartab.empty, i'), rec_consts);