src/HOL/Tools/inductive_package.ML
changeset 9804 ee0c337327cf
parent 9643 c94db1a96f4e
child 9831 9b883c416aef
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:49:51 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Sat Sep 02 21:50:38 2000 +0200
     1.3 @@ -877,7 +877,7 @@
     1.4    >> (Toplevel.theory o inductive_cases);
     1.5  
     1.6  val inductive_casesP =
     1.7 -  OuterSyntax.improper_command "inductive_cases"
     1.8 +  OuterSyntax.command "inductive_cases"
     1.9      "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
    1.10  
    1.11  val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];