--- a/src/Pure/Isar/toplevel.ML Mon Apr 17 14:03:51 2000 +0200
+++ b/src/Pure/Isar/toplevel.ML Mon Apr 17 14:04:46 2000 +0200
@@ -385,7 +385,7 @@
let
val _ =
if int orelse not int_only then ()
- else warning (command_msg "Executing interactive-only " tr);
+ else warning (command_msg "Interactive-only " tr);
val (result, opt_exn) =
(if ! trace then (writeln (command_msg "" tr); timeap) else I) (apply_trans int trans) state;
val _ = if int andalso print andalso not (! quiet) then print_state result else ();