# HG changeset patch
# User wenzelm
# Date 969028695 -7200
# Node ID d4af3f6fa9971bf7c84fd26917b0ea8a393ff11e
# Parent  32955afeb83529401227512619aa7eda009c413e
ML_command: no_timing;

diff -r 32955afeb835 -r d4af3f6fa997 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