--- a/src/Pure/Isar/isar_syn.ML Sat Mar 18 19:19:53 2000 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Mar 18 19:20:10 2000 +0100
@@ -379,7 +379,7 @@
(P.marg_comment >> IsarThy.skip_proof);
val forget_proofP =
- OuterSyntax.improper_command "oops" "forget proof" K.qed_global
+ OuterSyntax.command "oops" "forget proof" K.qed_global
(P.marg_comment >> IsarThy.forget_proof);
@@ -448,10 +448,6 @@
OuterSyntax.improper_command "undos_proof" "undo last proof commands" K.control
(P.nat >> (Toplevel.print oo IsarCmd.undos_proof));
-val kill_proofP =
- OuterSyntax.improper_command "kill_proof" "undo current proof" K.control
- (Scan.succeed IsarCmd.kill_proof);
-
val undoP =
OuterSyntax.improper_command "undo" "undo last command" K.control
(Scan.succeed (Toplevel.print o IsarCmd.undo));
@@ -643,7 +639,7 @@
nextP, qedP, terminal_proofP, immediate_proofP, default_proofP,
skip_proofP, forget_proofP, deferP, preferP, applyP, apply_endP,
proofP, alsoP, finallyP, backP, cannot_undoP, clear_undosP, redoP,
- undos_proofP, kill_proofP, undoP, killP,
+ undos_proofP, undoP, killP,
(*diagnostic commands*)
pretty_setmarginP, print_commandsP, print_contextP, print_theoryP,
print_syntaxP, print_theoremsP, print_attributesP, print_methodsP,