src/HOL/Tools/inductive.ML

   Outer_Syntax.local_theory @{command_spec "coinductive"} "define coinductive predicates"
     (ind_decl true);
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "inductive_cases"}
-    "create simplified instances of elimination rules (improper)"
+    "create simplified instances of elimination rules"
     (Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "inductive_simps"}
     "create simplification rules for inductive predicates"