--- a/ProgTutorial/Package/simple_inductive_package.ML	Sun Feb 19 01:33:47 2012 +0000
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Tue Mar 20 09:39:44 2012 +0000
@@ -21,7 +21,7 @@
 (* @chunk make_definitions *) 
 fun make_defs ((binding, syn), trm) lthy =
 let 
-  val arg = ((binding, syn), (Attrib.empty_binding, trm))
+  val arg = ((binding, syn), ((Binding.suffix_name "_def" binding, []), trm))
   val ((_, (_ , thm)), lthy) = Local_Theory.define arg lthy
 in 
   (thm, lthy) 
@@ -236,8 +236,8 @@
     (fn (((loc, preds), params), specs) =>
       Toplevel.local_theory loc (add_inductive preds params specs))
 
-val _ = Outer_Syntax.command "simple_inductive" "define inductive predicates"
-          Keyword.thy_decl specification
+val _ = Outer_Syntax.command ("simple_inductive", Keyword.thy_decl) "define inductive predicates"
+          specification
 (* @end *)
 
 end;