equal
deleted
inserted
replaced
13 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
13 (OuterKeyword.tag "TutorialML" OuterKeyword.thy_decl) |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
14 (OuterParse.ML_source >> (fn (txt, pos) => |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
15 Toplevel.generic_theory (ML_Context.exec (fn () => ML_Context.eval true pos txt)))); |
16 *} |
16 *} |
17 |
17 |
|
18 ML {* |
|
19 fun warning str = str |
|
20 fun tracing str = str |
|
21 *} |
18 |
22 |
19 end |
23 end |