src/Pure/Isar/isar_syn.ML

 val kill_proofP =
   OuterSyntax.improper_command "kill_proof" "abort current proof" K.control
     (Scan.succeed (Toplevel.print o Toplevel.proof_to_theory IsarThy.kill_proof));
 
 val qed_withP =
-  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes" K.qed
+  OuterSyntax.improper_command "qed_with" "conclude proof, may patch name and attributes"
+    K.qed_block
     (Scan.option P.name -- Scan.option P.attribs -- Scan.option (P.method -- P.interest)
       >> (uncurry IsarThy.global_qed_with));
 
 val qedP =
-  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed
+  OuterSyntax.command "qed" "conclude (sub-)proof" K.qed_block
     (Scan.option (P.method -- P.interest) >> IsarThy.qed);
 
 val terminal_proofP =
   OuterSyntax.command "by" "terminal backward proof" K.qed
     (P.method -- P.interest >> IsarThy.terminal_proof);

     (P.interest -- Scan.option (P.method -- P.interest)
       >> (Toplevel.print oo (Toplevel.proof o IsarThy.proof)));
 
 
 (* proof history *)
+
+val cannot_undoP =
+  OuterSyntax.improper_command "cannot_undo" "report 'cannot undo' error message" K.control
+    (P.name >> (Toplevel.print oo IsarCmd.cannot_undo));
 
 val clear_undoP =
   OuterSyntax.improper_command "clear_undo" "clear undo information" K.control
     (Scan.succeed (Toplevel.print o IsarCmd.clear_undo));
 

   print_ast_translationP, token_translationP, oracleP,
   (*proof commands*)
   theoremP, lemmaP, showP, haveP, thusP, henceP, assumeP, fixP, letP,
   thenP, fromP, factsP, beginP, endP, nextP, kill_proofP, qed_withP,
   qedP, terminal_proofP, immediate_proofP, default_proofP, refineP,
-  then_refineP, proofP, clear_undoP, undoP, redoP, undosP, backP,
-  prevP, upP, topP,
+  then_refineP, proofP, cannot_undoP, clear_undoP, undoP, redoP,
+  undosP, backP, prevP, upP, topP,
   (*diagnostic commands*)
   print_commandsP, print_theoryP, print_syntaxP, print_attributesP,
   print_methodsP, print_theoremsP, print_bindsP, print_lthmsP,
   print_thmsP, print_propP, print_termP, print_typeP,
   (*system commands*)