--- a/ProgTutorial/Helper/Command/Command.thy	Sat Jun 16 15:25:47 2012 +0100
+++ b/ProgTutorial/Helper/Command/Command.thy	Mon Jun 18 14:49:09 2012 +0100
@@ -9,7 +9,9 @@
    val do_nothing = Scan.succeed (Local_Theory.background_theory I)
    val kind = Keyword.thy_decl
 in
-   Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
+   Outer_Syntax.local_theory @{command_spec "foobar"} 
+     "description of foobar" 
+       do_nothing
 end
 *}
 
@@ -20,8 +22,9 @@
   val trace_prop_parser = Parse.prop >> trace_prop
   val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition"
-    trace_prop_parser
+  Outer_Syntax.local_theory @{command_spec "foobar_trace"} 
+    "traces a proposition"
+      trace_prop_parser
 end
 *}
 
@@ -36,8 +39,9 @@
    val prove_prop_parser = Parse.prop >> prove_prop
    val kind = Keyword.thy_goal
 in
-   Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proving a proposition"
-     prove_prop_parser
+   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_goal"} 
+     "proving a proposition"
+       prove_prop_parser
 end
 *}
 
@@ -64,8 +68,9 @@
    val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
  
 in
-   Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) "proving a proposition" 
-      (parser >> setup_proof)
+   Outer_Syntax.local_theory_to_proof @{command_spec "foobar_prove"} 
+     "proving a proposition" 
+        (parser >> setup_proof)
 end*}