src/HOL/Tools/datatype_package.ML

 
 (* outer syntax *)
 
 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));
 
 fun mk_datatype args =

     val names = map (fn ((((NONE, _), t), _), _) => t | ((((SOME t, _), _), _), _) => t) args;
     val specs = map (fn ((((_, vs), t), mx), cons) =>
       (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));
 
 
 val rep_datatype_decl =

     Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] --
     (P.$$$ "induction" |-- P.!!! SpecParse.xthm);
 
 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;
 
 
 end;