diff -r 8939b8fd8603 -r 069d525f8f1d ProgTutorial/Base.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ProgTutorial/Base.thy	Thu Mar 19 13:28:16 2009 +0100
@@ -0,0 +1,23 @@
+theory Base
+imports Main
+uses
+  "chunks.ML"
+  "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 "TutorialML" OuterKeyword.thy_decl)
+    (OuterParse.ML_source >> (fn (txt, pos) =>
+      Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt))));
+*}
+(*
+ML {*
+  fun warning str = str
+  fun tracing str = str
+*}
+*)
+end