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 "ProofGeneral.undo"
+     | "undostep"       => isarcmd "undos_proof 1" (* ProofGeneral.undo" *)
      | "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)