diff -r df7c3b1f390a -r 193b84a70ca4 src/HOL/Tools/datatype_aux.ML
--- a/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:17 2005 +0200
+++ b/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:18 2005 +0200
@@ -299,7 +299,7 @@
       Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
 
     fun get_dt_descr T i tname dts =
-      (case Symtab.lookup (dt_info, tname) of
+      (case Symtab.curried_lookup dt_info tname of
          NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
            \ nested recursion")
        | (SOME {index, descr, ...}) =>