src/HOL/Library/Binomial.thy
changeset 55143 04448228381d
parent 54703 499f92dc6e45
     1.1 --- a/src/HOL/Library/Binomial.thy	Sat Jan 25 21:52:04 2014 +0100
     1.2 +++ b/src/HOL/Library/Binomial.thy	Sat Jan 25 22:06:07 2014 +0100
     1.3 @@ -131,7 +131,7 @@
     1.4           prefer 4 apply (force simp add: constr_bij)
     1.5          prefer 3 apply force
     1.6         prefer 2 apply (blast intro: finite_Pow_iff [THEN iffD2]
     1.7 -         finite_subset [of _ "Pow (insert x F)", standard])
     1.8 +         finite_subset [of _ "Pow (insert x F)" for F])
     1.9        apply (blast intro: finite_Pow_iff [THEN iffD2, THEN [2] finite_subset])
    1.10        done
    1.11    qed