diff -r ce43c04d227d -r d94755882e36 ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Thu May 27 10:39:07 2010 +0200
@@ -61,12 +61,12 @@
 *}
 
 ML{*val spec_parser = 
-   OuterParse.fixes -- 
+   Parse.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))) []*}
 
 text {*
   which we explained in Section~\ref{sec:parsingspecs}.  There is no code included 
@@ -95,8 +95,8 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 (*<*)ML %no{*fun filtered_input str = 
-  filter OuterLex.is_proper (OuterSyntax.scan Position.none str) 
-fun parse p input = Scan.finite OuterLex.stopper (Scan.error p) input*}(*>*)
+  filter Token.is_proper (Outer_Syntax.scan Position.none str) 
+fun parse p input = Scan.finite Token.stopper (Scan.error p) input*}(*>*)
 text {*
   Note that in these definitions the parameter @{text R}, standing for the
   relation, is left implicit. For the moment we will ignore this kind
@@ -133,13 +133,13 @@
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
 
-val _ = OuterSyntax.local_theory "simple_inductive2" 
+val _ = Outer_Syntax.local_theory "simple_inductive2" 
           "definition of simple inductive predicates"
-             OuterKeyword.thy_decl specification*}
+             Keyword.thy_decl specification*}
 
 text {*
-  We call @{ML_ind  local_theory in OuterSyntax} with the kind-indicator 
-  @{ML_ind  thy_decl in OuterKeyword} since the package does not need to open 
+  We call @{ML_ind  local_theory in Outer_Syntax} with the kind-indicator 
+  @{ML_ind  thy_decl in Keyword} since the package does not need to open 
   up any proof (see Section~\ref{sec:newcommand}). 
   The auxiliary function @{text specification} in Lines 1 to 3
   gathers the information from the parser to be processed further