--- a/ProgTutorial/Package/Ind_Interface.thy	Fri Jun 03 15:15:17 2016 +0100
+++ b/ProgTutorial/Package/Ind_Interface.thy	Tue May 14 11:10:53 2019 +0200
@@ -62,7 +62,7 @@
 *}
 
 ML %grayML{*val spec_parser = 
-   Parse.fixes -- 
+   Parse.vars -- 
    Scan.optional 
      (Parse.$$$ "where" |--
         Parse.!!! 
@@ -96,7 +96,7 @@
 where
   accpartI: "(\<And>y. R y x \<Longrightarrow> accpart' y) \<Longrightarrow> accpart' x"
 (*<*)ML %no{*fun filtered_input str = 
-  filter Token.is_proper (Outer_Syntax.scan (Keyword.get_lexicons ()) Position.none str) 
+  filter Token.is_proper (Token.explode (Thy_Header.get_keywords' @{context}) 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
@@ -129,12 +129,12 @@
   done in Lines 5 to 7 in the code below.
 *}
 (*<*)ML %no{*fun add_inductive_cmd pred_specs rule_specs lthy = lthy 
-   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*)
-ML_val %linenosgray{*val specification : (local_theory -> local_theory) parser =
+   fun add_inductive pred_specs rule_specs lthy = lthy*}(*>*) (* FIXME: Is the dummy simple_inductive2 installed with ML, before there was ML_val*)
+ML %linenosgray{*val specification : (local_theory -> local_theory) parser =
   spec_parser >>
     (fn (pred_specs, rule_specs) => add_inductive_cmd pred_specs rule_specs)
 
-val _ = Outer_Syntax.local_theory @{command_spec "simple_inductive2"}
+val _ = Outer_Syntax.local_theory @{command_keyword "simple_inductive2"}
           "definition of simple inductive predicates"
              specification*}
 
@@ -152,19 +152,19 @@
   eventually will be).  Also the introduction rules are just strings. What we have
   to do first is to transform the parser's output into some internal
   datastructures that can be processed further. For this we can use the
-  function @{ML_ind  read_spec in Specification}. This function takes some strings
+  function @{ML_ind  read_multi_specs in Specification}. This function takes some strings
   (with possible typing annotations) and some rule specifications, and attempts
   to find a typing according to the given type constraints given by the 
   user and the type constraints by the ``ambient'' theory. It returns 
   the type for the predicates and also returns typed terms for the
   introduction rules. So at the heart of the function 
-  @{text "add_inductive_cmd"} is a call to @{ML read_spec in Specification}.
+  @{text "add_inductive_cmd"} is a call to @{ML read_multi_specs in Specification}.
 *}
 
 ML_val%grayML{*fun add_inductive_cmd pred_specs rule_specs lthy =
 let
   val ((pred_specs', rule_specs'), _) = 
-         Specification.read_spec pred_specs rule_specs lthy
+         Specification.read_multi_specs pred_specs rule_specs lthy
 in
   add_inductive pred_specs' rule_specs' lthy
 end*}