--- a/ProgTutorial/Parsing.thy	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/Parsing.thy	Sat Aug 28 13:27:16 2010 +0800
@@ -548,7 +548,7 @@
 
   you obtain a list consisting of only one command and two keyword tokens.
   If you want to see which keywords and commands are currently known to Isabelle, 
-  type:
+  use the function @{ML_ind get_lexicons in Keyword}:
 
 @{ML_response_fake [display,gray] 
 "let 
@@ -956,7 +956,7 @@
 *}
 
 ML{*let
-  val do_nothing = Scan.succeed (Local_Theory.theory I)
+  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
@@ -993,7 +993,7 @@
   \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
-  val do_nothing = Scan.succeed (Local_Theory.theory I)
+  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
@@ -1110,7 +1110,7 @@
   The crucial part of a command is the function that determines the behaviour
   of the command. In the code above we used a ``do-nothing''-function, which
   because of @{ML_ind succeed in Scan} does not parse any argument, but immediately
-  returns the simple function @{ML "Local_Theory.theory I"}. We can
+  returns the simple function @{ML "Local_Theory.background_theory I"}. We can
   replace this code by a function that first parses a proposition (using the
   parser @{ML Parse.prop}), then prints out the tracing
   information (using a new function @{text trace_prop}) and 
@@ -1119,7 +1119,7 @@
 
 ML{*let
   fun trace_prop str = 
-     Local_Theory.theory (fn ctxt => (tracing str; ctxt))
+     Local_Theory.background_theory (fn ctxt => (tracing str; ctxt))
 
   val kind = Keyword.thy_decl
 in