--- a/src/HOL/Tools/datatype_aux.ML Sun Jun 11 19:36:10 2006 +0200
+++ b/src/HOL/Tools/datatype_aux.ML Sun Jun 11 21:59:17 2006 +0200
@@ -307,7 +307,7 @@
\ nested recursion")
| (SOME {index, descr, ...}) =>
let val (_, vars, _) = (the o AList.lookup (op =) descr) index;
- val subst = ((map dest_DtTFree vars) ~~ dts) handle UnequalLengths =>
+ val subst = ((map dest_DtTFree vars) ~~ dts) handle Library.UnequalLengths =>
typ_error T ("Type constructor " ^ tname ^ " used with wrong\
\ number of arguments")
in (i + index, map (fn (j, (tn, args, cs)) => (i + j,