procedure SET_INDEX(FILE : in FILE_TYPE; TO : in POSITIVE_COUNT);

    Operates on a file of any mode. Sets the current index of the
    given file to the given index value (which may exceed the current
    size of the file).