--- a/ProgTutorial/Parsing.thy	Tue Mar 31 16:50:13 2009 +0100
+++ b/ProgTutorial/Parsing.thy	Tue Mar 31 20:31:18 2009 +0100
@@ -918,15 +918,16 @@
 
 ML{*let
   fun trace_top_lvl str = 
-     Toplevel.theory (fn thy => (tracing str; thy))
+     LocalTheory.theory (fn lthy => (tracing str; lthy))
 
   val trace_prop = OuterParse.prop >> trace_top_lvl
 
   val kind = OuterKeyword.thy_decl
 in
-  OuterSyntax.command "foobar" "traces a proposition" kind trace_prop
+  OuterSyntax.local_theory "foobar" "traces a proposition" kind trace_prop
 end *}
 
+
 text {*
   Now you can type