# HG changeset patch
# User wenzelm
# Date 955973086 -7200
# Node ID f745b34dcde379ff103782ccb027a3981d21647c
# Parent  453b493ece0a3bb221b9c308b16e9f8f9fbb490c
tuned msg;

diff -r 453b493ece0a -r f745b34dcde3 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Apr 17 14:03:51 2000 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Apr 17 14:04:46 2000 +0200
@@ -267,7 +267,7 @@
 fun assert_mode pred state =
   let val mode = get_mode state in
     if pred mode then state
-    else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)
+    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
   end;
 
 fun is_chain state = get_mode state = ForwardChain;
diff -r 453b493ece0a -r f745b34dcde3 src/Pure/Isar/toplevel.ML
--- 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 ();