--- a/ProgTutorial/Package/Ind_Interface.thy	Fri Jun 22 19:55:20 2012 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Mon Aug 27 10:24:10 2012 +0100
@@ -134,7 +134,7 @@
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
 
-val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl)
+val _ = Outer_Syntax.local_theory @{command_spec "simple_inductive2"}
           "definition of simple inductive predicates"
              specification*}