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