diff -r 6e6d9e80ebb4 -r e5b55d7be9bb src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
@@ -908,6 +908,8 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
+val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
+
 val datatype_decl =
   Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
     (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
@@ -919,7 +921,7 @@
       (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
   in snd o add_datatype false names specs end;
 
-val datatypeP =
+val _ =
   OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
     (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
 
@@ -932,14 +934,10 @@
 
 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
 
-val rep_datatypeP =
+val _ =
   OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
     (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
 
-
-val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
-val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
-
 end;