diff -r 30c957a74803 -r f29d4e507564 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Dec 17 17:41:32 1998 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Dec 17 17:45:51 1998 +0100
@@ -100,7 +100,7 @@
 datatype mode = Forward | ForwardChain | Backward;
 
 val mode_name =
-  fn Forward => "forward" | ForwardChain => "forward chain" | Backward => "backward";
+  fn Forward => "state" | ForwardChain => "chain" | Backward => "prove";
 
 
 (* type node *)