src/HOL/Tools/datatype_codegen.ML
changeset 17412 e26cb20ef0cc
parent 17261 193b84a70ca4
child 17521 0f1c48de39f5
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Thu Sep 15 17:16:55 2005 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Thu Sep 15 17:16:56 2005 +0200
     1.3 @@ -281,7 +281,7 @@
     1.4   |  _ => NONE);
     1.5  
     1.6  fun datatype_tycodegen thy defs gr dep module brack (Type (s, Ts)) =
     1.7 -      (case Symtab.curried_lookup (DatatypePackage.get_datatypes thy) s of
     1.8 +      (case Symtab.lookup (DatatypePackage.get_datatypes thy) s of
     1.9           NONE => NONE
    1.10         | SOME {descr, ...} =>
    1.11             if isSome (get_assoc_type thy s) then NONE else