Didn't know this vernacular command existed! That is quite superior: I will convert all local definitions to use Let, reserving Definition/Theorem/etc for names prefixed with Book_x_y