CookBook/Base.thy
changeset 106 bdd82350cf22
parent 80 95e9c4556221
child 160 cc9359bfacf4
--- a/CookBook/Base.thy	Mon Feb 09 01:12:00 2009 +0000
+++ b/CookBook/Base.thy	Mon Feb 09 01:23:35 2009 +0000
@@ -10,7 +10,7 @@
 
 val _ =
   OuterSyntax.command "ML" "eval ML text within theory"
-    (OuterKeyword.tag "CookBookML" OuterKeyword.thy_decl)
+    (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))));
 *}