--- 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 _ =