# HG changeset patch
# User wenzelm
# Date 1216027182 -7200
# Node ID 4bb03d4509e2854565571bd749498b55236d886d
# Parent  fc6d34e49e174fc02eb20a493f41954d190b5e6a
command 'redo' no longer available;

diff -r fc6d34e49e17 -r 4bb03d4509e2 src/Pure/ProofGeneral/proof_general_pgip.ML
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:41 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML	Mon Jul 14 11:19:42 2008 +0200
@@ -429,7 +429,7 @@
 fun isarcmd s = Isar.>>> (OuterSyntax.parse Position.none s);
 
 (* TODO:
-    - apply a command given a transition function, e.g. IsarCmd.undo.
+    - apply a command given a transition function;
     - fix position from path of currently open file [line numbers risk garbling though].
 *)
 
@@ -549,7 +549,7 @@
         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
-fun redostep _ = isarcmd "redo"
+fun redostep _ = sys_error "redo unavailable"
 
 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)