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;