diff -r f49dc7e96235 -r bdd82350cf22 CookBook/Base.thy --- 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)))); *}