clarified index antiquotation for ML: more ambitious type-setting, more accurate syntax;