It would be nice (for front ends) to be able to declare domains without a name, similarly to anoynomous axioms.