src/HOL/Library/Pocklington.thy

--- a/src/HOL/Library/Pocklington.thy	Tue Apr 28 19:15:50 2009 +0200
+++ b/src/HOL/Library/Pocklington.thy	Wed Apr 29 14:20:26 2009 +0200
@@ -568,7 +568,7 @@
 
 lemma nproduct_cmul:
   assumes fS:"finite S"
-  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult,recpower})* a(m)) S = c ^ (card S) * setprod a S"
+  shows "setprod (\<lambda>m. (c::'a::{comm_monoid_mult})* a(m)) S = c ^ (card S) * setprod a S"
 unfolding setprod_timesf setprod_constant[OF fS, of c] ..
 
 lemma coprime_nproduct: