updated builtin.theory; lifted arbitrary restriction on axiom definitions
(one can ignore symbols in the pattern, for instance skolem symbols)