src/Pure/Isar/isar_syn.ML

 val skip_proofP =
   OuterSyntax.improper_command "sorry" "skip proof (quick-and-dirty mode only!)" K.qed
     (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);
 
 
 
 (* proof steps *)

     (Scan.succeed (Toplevel.print o IsarCmd.redo));
 
 val undos_proofP =
   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));
 

   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, presumeP,
   defP, fixP, letP, caseP, thenP, fromP, withP, noteP, beginP, endP,
   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,
   thms_containingP, print_bindsP, print_lthmsP, print_casesP,
   print_thmsP, print_propP, print_termP, print_typeP,