--- a/ProgTutorial/Helper/Command/Command.thy	Sun Aug 22 22:56:52 2010 +0800
+++ b/ProgTutorial/Helper/Command/Command.thy	Sat Aug 28 13:27:16 2010 +0800
@@ -4,7 +4,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
@@ -14,7 +14,7 @@
 ML {*
 let
   fun trace_prop str =
-     Local_Theory.theory (fn lthy => (tracing str; lthy))
+     Local_Theory.background_theory (fn lthy => (tracing str; lthy))
   val trace_prop_parser = Parse.prop >> trace_prop
   val kind = Keyword.thy_decl
 in