A problem about the CLOCK

The followings are from gs51.pdf:

signal void one_thou_hz (void) {
while (1) { /* repeat forever */
PORT2 |= 1; /* set P1.2 */
twatch((CLOCK/2)/2000); /*delay for .0005 secs*/

PORT2 &= ~1; /* clear P1.2 */
twatch((CLOCK/2)/2000);
/*delayfor .0005 secs */
} /* repeat */
}

But I consider the delay is 0.00025 instead 0.0005,because (CLOCK/2)/2000*1/CLOCK= 1/4000
? Is it right?