"inductive_cases": proper command;

--- a/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:49:51 2000 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:50:38 2000 +0200
@@ -877,7 +877,7 @@
   >> (Toplevel.theory o inductive_cases);
 
 val inductive_casesP =
-  OuterSyntax.improper_command "inductive_cases"
+  OuterSyntax.command "inductive_cases"
     "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
 
 val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];