# HG changeset patch
# User wenzelm
# Date 1206475262 -3600
# Node ID e44c5a1a47bd3e0c5498b2786315fbb6b51c54bd
# Parent  9e0e4ce5131362d217d5221b6cb0d2e4c0f1bdc3
added 'ML_val' command (diagnostic);

diff -r 9e0e4ce51313 -r e44c5a1a47bd src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:01 2008 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Mar 25 21:01:02 2008 +0100
@@ -310,7 +310,11 @@
     (P.position P.text >> IsarCmd.use_mltext true);
 
 val _ =
-  OuterSyntax.command "ML_command" "eval ML text" (K.tag_ml K.diag)
+  OuterSyntax.command "ML_val" "eval ML text (diagnostic)" (K.tag_ml K.diag)
+    (P.position P.text >> IsarCmd.use_mltext true);
+
+val _ =
+  OuterSyntax.command "ML_command" "silently eval ML text (diagnostic)" (K.tag_ml K.diag)
     (P.position P.text >> (Toplevel.no_timing oo IsarCmd.use_mltext false));
 
 val _ =