The simplification procedure finite_Collect
has been deactivated after the Isabelle2013-2 release in changeset 31afce809794, because it sometimes behaves surprisingly or crashes. You can reactivate it with using [[simproc add: finite_Collect]]
between the lemma statement and the start of your proof. Then, your former proof works again.
By the way, it is in general not a good idea to use the repository version for your work unless you desparately need a new feature or want to participate in the Isabelle development process.