diff -r 4e7f5b22dd7d -r 80e3f43306cf src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Fri Apr 23 13:58:15 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Fri Apr 23 15:17:59 2010 +0200
@@ -555,7 +555,7 @@
 qed
 
 lemma setsum_mono2:
-fixes f :: "'a \<Rightarrow> 'b :: {ordered_ab_semigroup_add_imp_le,comm_monoid_add}"
+fixes f :: "'a \<Rightarrow> 'b :: ordered_comm_monoid_add"
 assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
 shows "setsum f A \<le> setsum f B"
 proof -
@@ -1030,7 +1030,7 @@
 lemma setprod_diff1: "finite A ==> f a \<noteq> 0 ==>
   (setprod f (A - {a}) :: 'a :: {field}) =
   (if a:A then setprod f A / f a else setprod f A)"
-by (erule finite_induct) (auto simp add: insert_Diff_if)
+  by (erule finite_induct) (auto simp add: insert_Diff_if)
 
 lemma setprod_inversef: 
   fixes f :: "'b \<Rightarrow> 'a::{field,division_by_zero}"