--- a/ProgTutorial/Base.thy	Mon May 24 20:02:11 2010 +0100
+++ b/ProgTutorial/Base.thy	Thu May 27 10:39:07 2010 +0200
@@ -98,9 +98,9 @@
 
 ML {*
 val _ =
-  OuterSyntax.command "ML" "eval ML text within theory"
-    (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl)
-    (OuterParse.position OuterParse.text >> 
+  Outer_Syntax.command "ML" "eval ML text within theory"
+    (Keyword.tag "TutorialML" Keyword.thy_decl)
+    (Parse.position Parse.text >> 
       (fn (txt, pos) =>
         Toplevel.generic_theory
          (ML_Context.exec 
@@ -108,35 +108,31 @@
               #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
 
 val _ =
-  OuterSyntax.command "ML_prf" "ML text within proof" 
-    (OuterKeyword.tag "TutorialML" OuterKeyword.prf_decl)
-    (OuterParse.ML_source >> (fn (txt, pos) =>
+  Outer_Syntax.command "ML_prf" "ML text within proof" 
+    (Keyword.tag "TutorialML" Keyword.prf_decl)
+    (Parse.ML_source >> (fn (txt, pos) =>
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> propagate_env_prf)))
 
 val _ =
-  OuterSyntax.command "ML_val" "diagnostic ML text" 
-  (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
-    (OuterParse.ML_source >> IsarCmd.ml_diag true)
+  Outer_Syntax.command "ML_val" "diagnostic ML text" 
+  (Keyword.tag "TutorialML" Keyword.diag)
+    (Parse.ML_source >> IsarCmd.ml_diag true)
 *}
 
 ML {*
 val _ =
-  OuterSyntax.command "setup" "ML theory setup" 
-    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
-      (OuterParse.ML_source >> (fn (txt, pos) => 
+  Outer_Syntax.command "setup" "ML theory setup" 
+    (Keyword.tag_ml Keyword.thy_decl)
+      (Parse.ML_source >> (fn (txt, pos) => 
         (Toplevel.theory (IsarCmd.global_setup (txt, pos) #> write_file_setup_blk txt))))
 *}
 
-ML {* Context.proof_map *}
-ML {* IsarCmd.local_setup ; Context.map_proof (write_file_lsetup_blk "") *}
-
-
 ML {*
 val _ =
-  OuterSyntax.local_theory "local_setup" "ML local theory setup" 
-    (OuterKeyword.tag_ml OuterKeyword.thy_decl)
-      (OuterParse.ML_source >> (fn (txt, pos) => 
+  Outer_Syntax.local_theory "local_setup" "ML local theory setup" 
+    (Keyword.tag_ml Keyword.thy_decl)
+      (Parse.ML_source >> (fn (txt, pos) => 
          IsarCmd.local_setup (txt, pos) #> write_file_lsetup_blk txt));
 *}