--- 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;