--- a/ProgTutorial/Parsing.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -939,7 +939,7 @@
 *}
 
 ML{*let
-  val do_nothing = Scan.succeed (LocalTheory.theory I)
+  val do_nothing = Scan.succeed (Local_Theory.theory I)
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.local_theory "foobar" "description of foobar" kind do_nothing
@@ -976,7 +976,7 @@
   \isacommand{ML}~@{text "\<verbopen>"}\\
   @{ML
 "let
-  val do_nothing = Scan.succeed (LocalTheory.theory I)
+  val do_nothing = Scan.succeed (Local_Theory.theory I)
   val kind = OuterKeyword.thy_decl
 in
   OuterSyntax.local_theory \"foobar\" \"description of foobar\" kind do_nothing
@@ -1093,7 +1093,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 "LocalTheory.theory I"}. We can
+  returns the simple function @{ML "Local_Theory.theory I"}. We can
   replace this code by a function that first parses a proposition (using the
   parser @{ML OuterParse.prop}), then prints out the tracing
   information (using a new function @{text trace_prop}) and 
@@ -1102,7 +1102,7 @@
 
 ML{*let
   fun trace_prop str = 
-     LocalTheory.theory (fn ctxt => (tracing str; ctxt))
+     Local_Theory.theory (fn ctxt => (tracing str; ctxt))
 
   val kind = OuterKeyword.thy_decl
 in
@@ -1181,14 +1181,14 @@
 text {*
   {\bf TBD below}
 
-  (FIXME: read a name and show how to store theorems; see @{ML_ind note in LocalTheory})
+  (FIXME: read a name and show how to store theorems; see @{ML_ind note in Local_Theory})
   
 *}
 
 ML_val{*val r = Unsynchronized.ref (NONE:(unit -> term) option)*}
 ML{*let
    fun after_qed thm_name thms lthy =
-        LocalTheory.note Thm.theoremK (thm_name, (flat thms)) lthy |> snd
+        Local_Theory.note (thm_name, (flat thms)) lthy |> snd
 
    fun setup_proof (thm_name, (txt, pos)) lthy =
    let