src/HOL/Tools/datatype_aux.ML
changeset 17261 193b84a70ca4
parent 16901 d649ff14096a
child 17412 e26cb20ef0cc
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:17 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Mon Sep 05 17:38:18 2005 +0200
     1.3 @@ -299,7 +299,7 @@
     1.4        Sign.string_of_typ sign (typ_of_dtyp (orig_descr @ descr) sorts T) ^ "\n" ^ msg);
     1.5  
     1.6      fun get_dt_descr T i tname dts =
     1.7 -      (case Symtab.lookup (dt_info, tname) of
     1.8 +      (case Symtab.curried_lookup dt_info tname of
     1.9           NONE => typ_error T (tname ^ " is not a datatype - can't use it in\
    1.10             \ nested recursion")
    1.11         | (SOME {index, descr, ...}) =>