diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Sun Feb 19 01:33:47 2012 +0000
+++ b/ProgTutorial/Parsing.thy	Tue Mar 20 09:39:44 2012 +0000
@@ -475,6 +475,9 @@
 ML{*type 'a parser = Token.T list -> 'a * Token.T list*}
 
 text {*
+  {\bf REDO!!}
+
+
   The reason for using token parsers is that theory syntax, as well as the
   parsers for the arguments of proof methods, use the type @{ML_type
   Token.T}.
@@ -506,10 +509,10 @@
   other syntactic category. The second indicates a space.
 
   We can easily change what is recognised as a keyword with the function
-  @{ML_ind keyword in Keyword}. For example calling it with 
+  @{ML_ind define in Keyword}. For example calling it with 
 *}
 
-ML{*val _ = Keyword.keyword "hello"*}
+ML{*val _ = Keyword.define ("hello", NONE) *}
 
 text {*
   then lexing @{text [quotes] "hello world"} will produce
@@ -960,7 +963,7 @@
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
   val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory "foobar" "description of foobar" kind do_nothing
+  Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
 end *}
 
 text {*
@@ -997,7 +1000,7 @@
   val do_nothing = Scan.succeed (Local_Theory.background_theory I)
   val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
+  Outer_Syntax.local_theory (\"foobar\", kind) \"description of foobar\" do_nothing
 end"}\\
   @{text "\<verbclose>"}\\
   \isacommand{end}
@@ -1098,10 +1101,10 @@
   nothing. The point of this command is only to show the procedure of how
   to interact with ProofGeneral. A similar procedure has to be done with any 
   other new command, and also any new keyword that is introduced with 
-  the function @{ML_ind keyword in Keyword}. For example:
+  the function @{ML_ind define in Keyword}. For example:
 *}
 
-ML{*val _ = Keyword.keyword "blink" *}
+ML{*val _ = Keyword.define ("blink", NONE) *}
 
 text {*
   At the moment the command \isacommand{foobar} is not very useful. Let us
@@ -1124,8 +1127,8 @@
 
   val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory "foobar_trace" "traces a proposition" 
-    kind (Parse.prop >> trace_prop)
+  Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition" 
+    (Parse.prop >> trace_prop)
 end *}
 
 text {*
@@ -1166,8 +1169,8 @@
   
   val kind = Keyword.thy_goal
 in
-  Outer_Syntax.local_theory_to_proof "foobar_goal" "proves a proposition" 
-    kind (Parse.prop >> goal_prop)
+  Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proves a proposition" 
+    (Parse.prop >> goal_prop)
 end *}
 
 text {*
@@ -1225,8 +1228,9 @@
    val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
  
 in
-   Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
-     Keyword.thy_goal (parser >> setup_proof)
+   Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) 
+     "proving a proposition" 
+       (parser >> setup_proof)
 end*}
 
 (*