--- a/ProgTutorial/Helper/Command/Command.thy	Wed Nov 18 14:06:01 2009 +0100
+++ b/ProgTutorial/Helper/Command/Command.thy	Thu Nov 19 14:11:50 2009 +0100
@@ -4,7 +4,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
@@ -14,7 +14,7 @@
 ML {*
 let
   fun trace_prop str =
-     LocalTheory.theory (fn lthy => (tracing str; lthy))
+     Local_Theory.theory (fn lthy => (tracing str; lthy))
   val trace_prop_parser = OuterParse.prop >> trace_prop
   val kind = OuterKeyword.thy_decl
 in
@@ -45,7 +45,7 @@
 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
@@ -65,7 +65,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 "simple_inductive" "description of foobar" kind do_nothing