diff -r 1aaa15ef731b -r 647cab4a72c2 ProgTutorial/Base.thy
--- a/ProgTutorial/Base.thy	Wed Apr 01 12:29:10 2009 +0100
+++ b/ProgTutorial/Base.thy	Wed Apr 01 15:42:47 2009 +0100
@@ -30,6 +30,11 @@
       Toplevel.proof (Proof.map_context (Context.proof_map
         (ML_Context.exec (fn () => ML_Context.eval true pos txt))) #> inherit_env_prf)))
 
+val _ =
+  OuterSyntax.command "ML_val" "diagnostic ML text" 
+  (OuterKeyword.tag "TutorialML" OuterKeyword.diag)
+    (OuterParse.ML_source >> IsarCmd.ml_diag true);
+
 *}
 (*
 ML {*