# HG changeset patch
# User wenzelm
# Date 950523824 -3600
# Node ID 07f25f7d2218de3976f43cf81b834ea028250807
# Parent  78fd6355ebb509854323b5079b2b91b1a3625c6e
tuned msg;

diff -r 78fd6355ebb5 -r 07f25f7d2218 src/Pure/Isar/proof.ML
--- 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;