author | wenzelm |
Thu, 03 Aug 2000 18:44:55 +0200 | |
changeset 9514 | 8cd9cfc22dd7 |
parent 9513 | 8531c18d9181 |
child 9515 | e6dfc9c9bf89 |
--- a/src/Pure/Interface/proof_general.ML Thu Aug 03 18:44:24 2000 +0200 +++ b/src/Pure/Interface/proof_general.ML Thu Aug 03 18:44:55 2000 +0200 @@ -212,7 +212,7 @@ (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); val undoP = - OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control + OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control (Scan.succeed (Toplevel.no_timing o IsarCmd.undo)); val context_thy_onlyP =