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 *)