changeset 17261 | 193b84a70ca4 |
parent 16901 | d649ff14096a |
child 17412 | e26cb20ef0cc |
--- 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, ...}) =>