ML_command: no_timing;
authorwenzelm
Fri, 15 Sep 2000 16:38:15 +0200 (2000-09-15)
changeset 9978 d4af3f6fa997
parent 9977 32955afeb835
child 9979 fd5053c8a7ac
ML_command: no_timing;
src/Pure/Isar/isar_syn.ML
--- 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