src/HOL/Tools/datatype_aux.ML
changeset 17412 e26cb20ef0cc
parent 17261 193b84a70ca4
child 17485 c39871c52977
     1.1 --- a/src/HOL/Tools/datatype_aux.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_aux.ML	Thu Sep 15 17:16:56 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.curried_lookup dt_info tname of
     1.8 +      (case Symtab.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, ...}) =>