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