src/Pure/ProofGeneral/proof_general_emacs.ML

 
 local structure P = OuterParse and K = OuterKeyword in
 
 fun undoP () = (*undo without output -- historical*)
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
+    (Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
 
 fun restartP () =
   OuterSyntax.improper_command "ProofGeneral.restart" "(internal)" K.control
     (P.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
 
 fun kill_proofP () =
   OuterSyntax.improper_command "ProofGeneral.kill_proof" "(internal)" K.control
-    (Scan.succeed (Toplevel.no_timing o IsarCmd.kill_proof_notify tell_clear_goals));
-
-fun isar_kill_proofP () =
-  OuterSyntax.improper_command "ProofGeneral.isar_kill_proof" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o
       Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
 
 fun inform_file_processedP () =
   OuterSyntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" K.control

   OuterSyntax.improper_command "ProofGeneral.process_pgip" "(internal)" K.control
     (P.text >> (Toplevel.no_timing oo
       (fn txt => Toplevel.imperative (fn () => ProofGeneralPgip.process_pgip txt))));
 
 fun init_outer_syntax () = List.app (fn f => f ())
-  [undoP, restartP, kill_proofP, isar_kill_proofP, inform_file_processedP,
-    inform_file_retractedP, process_pgipP];
+  [undoP, restartP, kill_proofP, inform_file_processedP, inform_file_retractedP, process_pgipP];
 
 end;
 
 
 (* init *)