src/ZF/Tools/datatype_package.ML

--- a/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/ZF/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -422,11 +422,9 @@
 
 val coind_prefix = if coind then "co" else "";
 
-val inductiveP = OuterSyntax.command (coind_prefix ^ "datatype")
+val _ = OuterSyntax.command (coind_prefix ^ "datatype")
   ("define " ^ coind_prefix ^ "datatype") K.thy_decl datatype_decl;
 
-val _ = OuterSyntax.add_parsers [inductiveP];
-
 end;
 
 end;