src/Pure/ProofGeneral/proof_general_pgip.ML

         val times = #times vs
     in
         isarcmd ("undos_proof " ^ Int.toString times)
     end
 
-fun redostep _ = sys_error "redo unavailable"
+fun redostep _ = raise Fail "redo unavailable"
 
 fun abortgoal _ = isarcmd "kill" (* was: ProofGeneral.kill_proof *)
 
 
 (*** PGIP identifier tables ***)