tuned msg;

--- a/src/Pure/Isar/proof.ML	Sun Feb 13 21:01:26 2000 +0100
+++ b/src/Pure/Isar/proof.ML	Mon Feb 14 11:23:44 2000 +0100
@@ -264,7 +264,7 @@
 fun assert_mode pred state =
   let val mode = get_mode state in
     if pred mode then state
-    else raise STATE ("Illegal application of proof command in " ^ mode_name mode ^ " mode", state)
+    else raise STATE ("Illegal application of command in " ^ mode_name mode ^ " mode", state)
   end;
 
 fun is_chain state = get_mode state = ForwardChain;