src/Pure/proof_general.ML

      | "comment"	=> isarscript data  (* NB: should be ignored, but process anyway *)
      | "litcomment"     => isarscript data
      | "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? *)
      (* proofctxt: improper commands *)
      | "askids"         => askids (thyname_attro attrs, objtype_attro attrs)

 			      val thyname = topthy_name()
 			   in (isarscript data;
 			       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)
      | "openfile"       => (inform_file_retracted (fileurl_of attrs);
 			    currently_open_file := Some (fileurl_of attrs))