src/HOL/Tools/inductive.ML

--- a/src/HOL/Tools/inductive.ML	Mon Nov 26 13:54:43 2012 +0100
+++ b/src/HOL/Tools/inductive.ML	Mon Nov 26 14:43:28 2012 +0100
@@ -1157,7 +1157,7 @@
 
 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 _ =