Change oddly-chosen OID allocation.

 Change oddly-chosen OID allocation.
 
 I noticed while fooling with John Naylor's bootstrap-data patch that we had
 one high-numbered manually assigned OID, 8888, which evidently came from a
 submission that the committer didn't bother to bring into line with usual
 OID allocation practices before committing.  That's a bad idea, because it
 creates a hazard for other patches that may be temporarily using high OID
 numbers.  Change it to something more in line with what we usually do.
 
 This evidently dates to commit abb173392.  It's too late to change it
 in released branches, but we can fix it in HEAD.