diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Package/simple_inductive_package.ML --- a/ProgTutorial/Package/simple_inductive_package.ML Fri Jun 22 19:55:20 2012 +0100 +++ b/ProgTutorial/Package/simple_inductive_package.ML Mon Aug 27 10:24:10 2012 +0100 @@ -236,7 +236,7 @@ (fn (((loc, preds), params), specs) => Toplevel.local_theory loc (add_inductive preds params specs)) -val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates" +val _ = Outer_Syntax.command @{command_spec "simple_inductive"} "define inductive predicates" specification (* @end *)