--- a/CookBook/Base.thy	Thu Jan 08 22:46:06 2009 +0000
+++ b/CookBook/Base.thy	Thu Jan 08 22:47:15 2009 +0000
@@ -5,4 +5,14 @@
   "antiquote_setup.ML"
 begin
 
+(* to have a special tag for text enclosed in ML *)
+ML {*
+
+val _ =
+  OuterSyntax.command "ML" "eval ML text within theory"
+    (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl)
+    (OuterParse.ML_source >> (fn (txt, pos) =>
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
+*}
+
 end