made command 'undo' silent ('ProofGeneral.undo' becomes a historical relic);

--- a/src/Pure/Isar/isar_syn.ML	Thu Oct 25 13:52:05 2007 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Oct 25 16:57:57 2007 +0200
@@ -731,7 +731,7 @@
 
 val _ =
   OuterSyntax.improper_command "undo" "undo last command" K.control
-    (Scan.succeed (Toplevel.no_timing o Toplevel.print o IsarCmd.undo));
+    (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));
 
 val _ =
   OuterSyntax.improper_command "kill" "kill current history node" K.control

--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Oct 25 13:52:05 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Thu Oct 25 16:57:57 2007 +0200
@@ -231,7 +231,7 @@
 
 local structure P = OuterParse and K = OuterKeyword in
 
-fun undoP () = (*undo without output*)
+fun undoP () = (*undo without output -- historical*)
   OuterSyntax.improper_command "ProofGeneral.undo" "(internal)" K.control
     (Scan.succeed (Toplevel.no_timing o IsarCmd.undo));