diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Helper/Command/Command.thy
--- a/ProgTutorial/Helper/Command/Command.thy	Sun Feb 19 01:33:47 2012 +0000
+++ b/ProgTutorial/Helper/Command/Command.thy	Tue Mar 20 09:39:44 2012 +0000
@@ -1,5 +1,7 @@
 theory Command
 imports Main
+keywords "foobar" "foobar_trace" :: thy_decl and
+         "foobar_goal" "foobar_prove" :: thy_goal
 begin
 
 ML {*
@@ -7,7 +9,7 @@
    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
+   Outer_Syntax.local_theory ("foobar", kind) "description of foobar" do_nothing
 end
 *}
 
@@ -18,8 +20,8 @@
   val trace_prop_parser = Parse.prop >> trace_prop
   val kind = Keyword.thy_decl
 in
-  Outer_Syntax.local_theory "foobar_trace" "traces a proposition"
-    kind trace_prop_parser
+  Outer_Syntax.local_theory ("foobar_trace", kind) "traces a proposition"
+    trace_prop_parser
 end
 *}
 
@@ -34,8 +36,8 @@
    val prove_prop_parser = Parse.prop >> prove_prop
    val kind = Keyword.thy_goal
 in
-   Outer_Syntax.local_theory_to_proof "foobar_goal" "proving a proposition"
-     kind prove_prop_parser
+   Outer_Syntax.local_theory_to_proof ("foobar_goal", kind) "proving a proposition"
+     prove_prop_parser
 end
 *}
 
@@ -62,8 +64,8 @@
    val parser = Parse_Spec.opt_thm_name ":" -- Parse.ML_source
  
 in
-   Outer_Syntax.local_theory_to_proof "foobar_prove" "proving a proposition" 
-     Keyword.thy_goal (parser >> setup_proof)
+   Outer_Syntax.local_theory_to_proof ("foobar_prove", Keyword.thy_goal) "proving a proposition" 
+      (parser >> setup_proof)
 end*}