# HG changeset patch
# User wenzelm
# Date 924778990 -7200
# Node ID b0448cab1b1e11e95e3a95006cbdfc17edca5912
# Parent  48f90bc10cf5cff3ce695d96c597b6eea1eedee6
rep_datatype syntax: 'induction' instead of 'induct';

diff -r 48f90bc10cf5 -r b0448cab1b1e src/HOL/Tools/datatype_package.ML
--- a/src/HOL/Tools/datatype_package.ML	Thu Apr 22 12:50:39 1999 +0200
+++ b/src/HOL/Tools/datatype_package.ML	Thu Apr 22 13:03:10 1999 +0200
@@ -686,7 +686,7 @@
   Scan.option (Scan.repeat1 name) --
     Scan.optional ($$$ "distinct" |-- !!! (and_list1 xthms1)) [] --
     Scan.optional ($$$ "inject" |-- !!! (and_list1 xthms1)) [] --
-    ($$$ "induct" |-- !!! xthm);
+    ($$$ "induction" |-- !!! xthm);
 
 fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #1 o rep_datatype opt_ts dss iss ind;
 
@@ -695,7 +695,7 @@
     (rep_datatype_decl >> (Toplevel.theory o mk_rep_datatype));
 
 
-val _ = OuterSyntax.add_keywords ["distinct", "inject", "induct"];
+val _ = OuterSyntax.add_keywords ["distinct", "inject", "induction"];
 val _ = OuterSyntax.add_parsers [datatypeP, rep_datatypeP];
 
 end;