--- a/src/Tools/eqsubst.ML Fri Nov 26 22:04:33 2010 +0100
+++ b/src/Tools/eqsubst.ML Fri Nov 26 22:29:41 2010 +0100
@@ -235,13 +235,13 @@
val initenv =
Envir.Envir {maxidx = ix2, tenv = Vartab.empty, tyenv = typinsttab};
val useq = Unify.smash_unifiers thry [a] initenv
- handle UnequalLengths => Seq.empty
+ handle ListPair.UnequalLengths => Seq.empty
| Term.TERM _ => Seq.empty;
fun clean_unify' useq () =
(case (Seq.pull useq) of
NONE => NONE
| SOME (h,t) => SOME (mk_insts h, Seq.make (clean_unify' t)))
- handle UnequalLengths => NONE
+ handle ListPair.UnequalLengths => NONE
| Term.TERM _ => NONE
in
(Seq.make (clean_unify' useq))