--- 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 *)