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