Allow adding only constant (as opposed to schematic) symbols to a running theory

This commit introduces the separation between Function/Predicate labels and
theory symbols. Both constant and schematic function labels behave as functions,
both constant and schematic predicate labels behave as predicates, but only
constant function and predicate labels can be symbols in a theory. This is now
expressed in the project by a marker trait TheorySymbol.