1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:41:22 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sat Oct 06 16:50:04 2007 +0200
     1.3 @@ -908,6 +908,8 @@
     1.4  
     1.5  local structure P = OuterParse and K = OuterKeyword in
     1.6  
     1.7 +val _ = OuterSyntax.keywords ["distinct", "inject", "induction"];
     1.8 +
     1.9  val datatype_decl =
    1.10    Scan.option (P.$$$ "(" |-- P.name --| P.$$$ ")") -- P.type_args -- P.name -- P.opt_infix --
    1.11      (P.$$$ "=" |-- P.enum1 "|" (P.name -- Scan.repeat P.typ -- P.opt_mixfix));
    1.12 @@ -919,7 +921,7 @@
    1.13        (vs, t, mx, map (fn ((x, y), z) => (x, y, z)) cons)) args;
    1.14    in snd o add_datatype false names specs end;
    1.15  
    1.16 -val datatypeP =
    1.17 +val _ =
    1.18    OuterSyntax.command "datatype" "define inductive datatypes" K.thy_decl
    1.19      (P.and_list1 datatype_decl >> (Toplevel.theory o mk_datatype));
    1.20  
    1.21 @@ -932,14 +934,10 @@
    1.22  
    1.23  fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind;
    1.24  
    1.25 -val rep_datatypeP =
    1.26 +val _ =
    1.27    OuterSyntax.command "rep_datatype" "represent existing types inductively" K.thy_decl
    1.28      (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
    1.29  
    1.30 -
    1.31 -val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
    1.32 -val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
    1.33 -
    1.34  end;
    1.35  
    1.36