# HG changeset patch
# User wenzelm
# Date 966539245 -7200
# Node ID c94db1a96f4ec43a87aa4cce84cfed9c6949f9ea
# Parent  d8d1f70024bdef67820114c4dfb56eecf55a8ba0
removed obsolete keyword;

diff -r d8d1f70024bd -r c94db1a96f4e src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:06:04 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:07:25 2000 +0200
@@ -880,7 +880,7 @@
   OuterSyntax.improper_command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
 
-val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"];
+val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
 val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
 
 end;