Instantiated subst rule to avoid problems with HO unification.

--- a/src/HOL/Equiv_Relations.thy	Tue May 06 23:33:05 2008 +0200
+++ b/src/HOL/Equiv_Relations.thy	Wed May 07 10:56:33 2008 +0200
@@ -316,7 +316,7 @@
 lemma equiv_imp_dvd_card:
   "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
     ==> k dvd card A"
-  apply (rule Union_quotient [THEN subst])
+  apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]])
    apply assumption
   apply (rule dvd_partition)
      prefer 3 apply (blast dest: quotient_disj)