# HG changeset patch
# User wenzelm
# Date 953403610 -3600
# Node ID 4e42e1734004ee40b89bfeb906e86a3a7a2b8929
# Parent  b6dd80ea3af1773ae7b8e70fb40f4ecd706ce80b
'oops' made proper;
removed 'kill_proof' (superceded by 'kill');

diff -r b6dd80ea3af1 -r 4e42e1734004 src/Pure/Isar/isar_syn.ML
--- 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,