removed obsolete keyword;
authorwenzelm
Thu Aug 17 21:07:25 2000 +0200 (2000-08-17)
changeset 9643c94db1a96f4e
parent 9642 d8d1f70024bd
child 9644 6b0b6b471855
removed obsolete keyword;
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:06:04 2000 +0200
     1.2 +++ b/src/HOL/Tools/inductive_package.ML	Thu Aug 17 21:07:25 2000 +0200
     1.3 @@ -880,7 +880,7 @@
     1.4    OuterSyntax.improper_command "inductive_cases"
     1.5      "create simplified instances of elimination rules (improper)" K.thy_script ind_cases;
     1.6  
     1.7 -val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs", "of"];
     1.8 +val _ = OuterSyntax.add_keywords ["intros", "monos", "con_defs"];
     1.9  val _ = OuterSyntax.add_parsers [inductiveP, coinductiveP, inductive_casesP];
    1.10  
    1.11  end;