--- a/ProgTutorial/Package/simple_inductive_package.ML	Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Package/simple_inductive_package.ML	Thu May 27 10:39:07 2010 +0200
@@ -220,14 +220,14 @@
 
 (* @chunk parser *)
 val spec_parser = 
-   OuterParse.opt_target --
-   OuterParse.fixes -- 
-   OuterParse.for_fixes --
+   Parse.opt_target --
+   Parse.fixes -- 
+   Parse.for_fixes --
    Scan.optional 
-     (OuterParse.$$$ "where" |--
-        OuterParse.!!! 
-          (OuterParse.enum1 "|" 
-             (SpecParse.opt_thm_name ":" -- OuterParse.prop))) []
+     (Parse.$$$ "where" |--
+        Parse.!!! 
+          (Parse.enum1 "|" 
+             (Parse_Spec.opt_thm_name ":" -- Parse.prop))) []
 (* @end *)
 
 (* @chunk syntax *)
@@ -236,8 +236,8 @@
     (fn (((loc, preds), params), specs) =>
       Toplevel.local_theory loc (add_inductive preds params specs))
 
-val _ = OuterSyntax.command "simple_inductive" "define inductive predicates"
-          OuterKeyword.thy_decl specification
+val _ = Outer_Syntax.command "simple_inductive" "define inductive predicates"
+          Keyword.thy_decl specification
 (* @end *)
 
 end;