diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Sun Feb 19 01:33:47 2012 +0000 +++ b/ProgTutorial/Package/Ind_Interface.thy Tue Mar 20 09:39:44 2012 +0000 @@ -1,5 +1,6 @@ theory Ind_Interface imports Ind_Intro Simple_Inductive_Package +keywords "simple_inductive2" :: thy_decl begin section {* Parsing and Typing the Specification\label{sec:interface} *} @@ -133,9 +134,9 @@ spec_parser >> (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs) -val _ = Outer_Syntax.local_theory "simple_inductive2" +val _ = Outer_Syntax.local_theory ("simple_inductive2", Keyword.thy_decl) "definition of simple inductive predicates" - Keyword.thy_decl specification*} + specification*} text {* We call @{ML_ind local_theory in Outer_Syntax} with the kind-indicator