Instantiated subst rule to avoid problems with HO unification.
authorberghofe
Wed May 07 10:56:33 2008 +0200 (2008-05-07)
changeset 267913581a9c71909
parent 26790 e8cc166ba123
child 26792 f2d75fd23124
Instantiated subst rule to avoid problems with HO unification.
src/HOL/Equiv_Relations.thy
     1.1 --- a/src/HOL/Equiv_Relations.thy	Tue May 06 23:33:05 2008 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed May 07 10:56:33 2008 +0200
     1.3 @@ -316,7 +316,7 @@
     1.4  lemma equiv_imp_dvd_card:
     1.5    "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
     1.6      ==> k dvd card A"
     1.7 -  apply (rule Union_quotient [THEN subst])
     1.8 +  apply (rule Union_quotient [THEN subst [where P="\<lambda>A. k dvd card A"]])
     1.9     apply assumption
    1.10    apply (rule dvd_partition)
    1.11       prefer 3 apply (blast dest: quotient_disj)