diff -r 1c4250bc6258 -r 780100cd4060 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Mon Nov 07 10:49:25 2011 +0000
+++ b/ProgTutorial/Base.thy	Mon Nov 07 13:36:07 2011 +0000
@@ -101,10 +101,11 @@
            (fn () => ML_Context.eval_text true pos txt) 
               #> propagate_env #> Context.map_theory (write_file_ml_blk txt))))
 *}
+
 ML {*
 val _ =
   Outer_Syntax.command "ML_prf" "ML text within proof" 
-    (Keyword.tag "TutorialML" Keyword.prf_decl)
+    (Keyword.tag "TutorialMLprf" Keyword.prf_decl)
     (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)))