--- a/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Nominal/nominal_package.ML Sat Oct 06 16:50:04 2007 +0200
@@ -2094,12 +2094,10 @@
(vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
in add_nominal_datatype false names specs end;
-val nominal_datatypeP =
+val _ =
OuterSyntax.command "nominal_datatype" "define inductive datatypes" K.thy_decl
(P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
-val _ = OuterSyntax.add_parsers [nominal_datatypeP];
-
end;
end