1.1 --- a/src/Tools/eqsubst.ML	Fri Nov 26 22:04:33 2010 +0100
     1.2 +++ b/src/Tools/eqsubst.ML	Fri Nov 26 22:29:41 2010 +0100
     1.3 @@ -235,13 +235,13 @@
     1.4            val initenv =
     1.5              Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
     1.6            val useq = Unify.smash_unifiers thry [a] initenv
     1.7 -              handle UnequalLengths => Seq.empty
     1.8 +              handle ListPair.UnequalLengths => Seq.empty
     1.9                     | Term.TERM _ => Seq.empty;
    1.10            fun clean_unify' useq () =
    1.11                (case (Seq.pull useq) of
    1.12                   NONE => NONE
    1.13                 | SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
    1.14 -              handle UnequalLengths => NONE
    1.15 +              handle ListPair.UnequalLengths => NONE
    1.16                     | Term.TERM _ => NONE
    1.17          in
    1.18            (Seq.make (clean_unify' useq))