--- a/ProgTutorial/Parsing.thy	Mon Mar 30 17:40:20 2009 +0200
+++ b/ProgTutorial/Parsing.thy	Wed Apr 01 14:50:09 2009 +0200
@@ -919,15 +919,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