diff -r 98e6a0a011f3 -r 7dc7dcd63224 src/HOL/Tools/datatype_codegen.ML
--- a/src/HOL/Tools/datatype_codegen.ML	Tue Jan 17 10:26:50 2006 +0100
+++ b/src/HOL/Tools/datatype_codegen.ML	Tue Jan 17 16:36:57 2006 +0100
@@ -306,8 +306,6 @@
     DatatypePackage.get_all_datatype_cons,
   CodegenPackage.add_defgen
     ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
-  CodegenPackage.add_defgen
-    ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons),
   CodegenPackage.ensure_datatype_case_consts
     DatatypePackage.get_datatype_case_consts
     DatatypePackage.get_case_const_data