src/HOL/Tools/Datatype/datatype_aux.ML

       (case Symtab.lookup dt_info tname of
          NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
            \ nested recursion")
        | (SOME {index, descr, ...}) =>
            let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
-               val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
+               val subst = ((map dest_DtTFree vars) ~~ dts) handle ListPair.UnequalLengths =>
                  typ_error T ("Type constructor " ^ tname ^ " used with wrong\
                   \ number of arguments")
            in (i + index, map (fn (j, (tn, args, cs)) => (i + j,
              (tn, map (subst_DtTFree i subst) args,
               map (apsnd (map (subst_DtTFree i subst))) cs))) descr)