Bug fix (w/test case) for ThmSetData's new way to add theorems

Problem was that the callback function attached to the set didn't get
called, even though the theorem was successfully exported. This meant
that a set like "simp" (which feeds into srw_ss()) didn't prompt any
change to the stateful simpset. Being successfully exported did at
least mean that the theorem would get into the simpset in descendent
theories.
More (automatic) rewrites about bag disjointness.
More simple rewrites (most automatic) about bags.
Useful results about the multiset ordering relation.