# HG changeset patch
# User aspinall
# Date 1100523103 -3600
# Node ID b084384960d10dd624d2a1c4299f1ae74571317f
# Parent  ce83b7e74a9181b44d5d32596e745619446a7e07
Add <undoitem> for theory-state undos.

diff -r ce83b7e74a91 -r b084384960d1 src/Pure/proof_general.ML
--- a/src/Pure/proof_general.ML	Mon Nov 15 12:13:14 2004 +0100
+++ b/src/Pure/proof_general.ML	Mon Nov 15 13:51:43 2004 +0100
@@ -1168,7 +1168,7 @@
      | "spuriouscmd"    => isarscript data
      | "badcmd"		=> isarscript data
      (* improperproofcmd: improper commands which *do not* belong in script *)
-     | "undostep"       => isarcmd "undos_proof 1" (* ProofGeneral.undo" *)
+     | "undostep"       => isarcmd "undos_proof 1"
      | "abortgoal"      => isarcmd "ProofGeneral.kill_proof"  
      | "forget"         => error "Not implemented" 
      | "restoregoal"    => error "Not implemented"  (* could just treat as forget? *)
@@ -1190,6 +1190,7 @@
 			       writeln ("Theory \""^thyname^"\" completed."))
 			   end
      (* improperfilecmd: theory-level commands not in script *)
+     | "undoitem"       => isarcmd "ProofGeneral.undo"
      | "aborttheory"    => isarcmd ("init_toplevel")
      | "retracttheory"  => isarcmd ("kill_thy " ^ (quote (thyname_attr attrs)))
      | "loadfile"       => use_thy_or_ml_file (fileurl_of attrs)