diff -r 0760fdf56942 -r 5734ab5dd86d ProgTutorial/Package/Ind_Interface.thy --- 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*}