diff -r f223f8223d4a -r 7e25716c3744 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Sun Feb 19 01:33:47 2012 +0000
+++ b/ProgTutorial/Base.thy	Tue Mar 20 09:39:44 2012 +0000
@@ -1,6 +1,9 @@
 theory Base
 imports Main 
         "~~/src/HOL/Library/LaTeXsugar"
+keywords "ML" "setup" "local_setup" :: thy_decl and
+         "ML_prf" :: prf_decl and
+         "ML_val" :: diag
 uses
   ("output_tutorial.ML")
   ("antiquote_setup.ML")
@@ -92,8 +95,7 @@
 
 ML {*
 val _ =
-  Outer_Syntax.command "ML" "eval ML text within theory"
-    (Keyword.tag "TutorialML" Keyword.thy_decl)
+  Outer_Syntax.command ("ML", Keyword.tag "TutorialML" Keyword.thy_decl) "eval ML text within theory"
     (Parse.position Parse.text >> 
       (fn (txt, pos) =>
         Toplevel.generic_theory
@@ -104,8 +106,7 @@
 
 ML {*
 val _ =
-  Outer_Syntax.command "ML_prf" "ML text within proof" 
-    (Keyword.tag "TutorialMLprf" Keyword.prf_decl)
+  Outer_Syntax.command ("ML_prf", Keyword.tag "TutorialMLprf" Keyword.prf_decl) "ML text within proof" 
     (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> propagate_env_prf)))
@@ -113,23 +114,20 @@
 
 ML {*
 val _ =
-  Outer_Syntax.command "ML_val" "diagnostic ML text" 
-  (Keyword.tag "TutorialML" Keyword.diag)
+  Outer_Syntax.command ("ML_val", Keyword.tag "TutorialML" Keyword.diag) "diagnostic ML text" 
     (Parse.ML_source >> Isar_Cmd.ml_diag true)
 *}
 
 ML {*
 val _ =
-  Outer_Syntax.command "setup" "ML theory setup" 
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup" 
       (Parse.ML_source >> (fn (txt, pos) => 
         (Toplevel.theory (Isar_Cmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
 *}
 
 ML {*
 val _ =
-  Outer_Syntax.local_theory "local_setup" "ML local theory setup" 
-    (Keyword.tag_ml Keyword.thy_decl)
+  Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup" 
       (Parse.ML_source >> (fn (txt, pos) => 
          Isar_Cmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}