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)))); *}