# HG changeset patch
# User wenzelm
# Date 954612592 -7200
# Node ID 656f1b61875a72484940f19a3a50f5b949a80b38
# Parent  1a2c5ccebfdb7a4d58623ca703f6f4e72dd42dc2
added ProofGeneral.undo;

diff -r 1a2c5ccebfdb -r 656f1b61875a src/Pure/Interface/proof_general.ML
--- a/src/Pure/Interface/proof_general.ML	Sat Apr 01 20:09:20 2000 +0200
+++ b/src/Pure/Interface/proof_general.ML	Sat Apr 01 20:09:52 2000 +0200
@@ -205,10 +205,14 @@
 
 local structure P = OuterParse and K = OuterSyntax.Keyword in
 
-val silent_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
+val old_undoP =	(* FIXME same name for compatibility with PG/Isabelle99 *)
   OuterSyntax.improper_command "undo" "undo last command (no output)" K.control
     (Scan.succeed IsarCmd.undo);
 
+val undoP =
+  OuterSyntax.improper_command "ProofGeneral.undo" "undo last command (no output)" K.control
+    (Scan.succeed IsarCmd.undo);
+
 val context_thy_onlyP =
   OuterSyntax.improper_command "ProofGeneral.context_thy_only" "(internal)" K.control
     (P.name >> IsarThy.init_context update_thy_only);
@@ -234,7 +238,7 @@
     (P.name >> (fn name => Toplevel.imperative (fn () => inform_file_retracted name)));
 
 fun init_outer_syntax () = OuterSyntax.add_parsers
- [silent_undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
+ [old_undoP, undoP, restartP, kill_proofP, context_thy_onlyP, try_context_thy_onlyP,
   inform_file_processedP, inform_file_retractedP];
 
 end;