author | wenzelm |
Fri, 15 Sep 2000 16:38:15 +0200 (2000-09-15) | |
changeset 9978 | d4af3f6fa997 |
parent 9977 | 32955afeb835 |
child 9979 | fd5053c8a7ac |
--- a/src/Pure/Isar/isar_syn.ML Fri Sep 15 16:31:36 2000 +0200 +++ b/src/Pure/Isar/isar_syn.ML Fri Sep 15 16:38:15 2000 +0200 @@ -228,7 +228,7 @@ val ml_commandP = OuterSyntax.command "ML_command" "eval ML text" K.diag - (P.text -- P.marg_comment >> IsarCmd.use_mltext false); + (P.text -- P.marg_comment >> (Toplevel.no_timing oo IsarCmd.use_mltext false)); val ml_setupP = OuterSyntax.command "ML_setup" "eval ML text (may change theory)" K.thy_decl