diff -r 693711a0c702 -r e0d368a45537 CookBook/Package/simple_inductive_package.ML --- a/CookBook/Package/simple_inductive_package.ML Sat Feb 21 11:38:14 2009 +0000 +++ b/CookBook/Package/simple_inductive_package.ML Sun Feb 22 03:44:03 2009 +0000 @@ -191,13 +191,13 @@ (* @end *) (* @chunk syntax *) -val ind_decl = +val specification = spec_parser >> (fn (((loc, preds), params), specs) => Toplevel.local_theory loc (add_inductive preds params specs)) val _ = OuterSyntax.command "simple_inductive" "define inductive predicates" - OuterKeyword.thy_decl ind_decl + OuterKeyword.thy_decl specification (* @end *) end;