diff -r a643fcbc3468 -r eedbb8d22ca2 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 15:44:20 2004 +0100
@@ -320,6 +320,16 @@
     apply (simp_all add: Union_quotient equiv_type finite_quotient)
   done
 
+lemma card_quotient_disjoint:
+ "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
+apply(simp add:quotient_def)
+apply(subst card_UN_disjoint)
+   apply assumption
+  apply simp
+ apply(fastsimp simp add:inj_on_def)
+apply (simp add:setsum_constant_nat)
+done
+
 ML
 {*
 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";