diff -r f9b43d197d16 -r 080b755377c0 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue May 04 08:55:39 2010 +0200
+++ b/src/HOL/Big_Operators.thy	Tue May 04 08:55:43 2010 +0200
@@ -33,7 +33,7 @@
 text {* for ad-hoc proofs for @{const fold_image} *}
 
 lemma (in comm_monoid_add) comm_monoid_mult:
-  "comm_monoid_mult (op +) 0"
+  "class.comm_monoid_mult (op +) 0"
 proof qed (auto intro: add_assoc add_commute)
 
 notation times (infixl "*" 70)
@@ -1200,7 +1200,8 @@
 context semilattice_inf
 begin
 
-lemma ab_semigroup_idem_mult_inf: "ab_semigroup_idem_mult inf"
+lemma ab_semigroup_idem_mult_inf:
+  "class.ab_semigroup_idem_mult inf"
 proof qed (rule inf_assoc inf_commute inf_idem)+
 
 lemma fold_inf_insert[simp]: "finite A \<Longrightarrow> fold inf b (insert a A) = inf a (fold inf b A)"
@@ -1270,7 +1271,7 @@
 context semilattice_sup
 begin
 
-lemma ab_semigroup_idem_mult_sup: "ab_semigroup_idem_mult sup"
+lemma ab_semigroup_idem_mult_sup: "class.ab_semigroup_idem_mult sup"
 by (rule semilattice_inf.ab_semigroup_idem_mult_inf)(rule dual_semilattice)
 
 lemma fold_sup_insert[simp]: "finite A \<Longrightarrow> fold sup b (insert a A) = sup a (fold sup b A)"
@@ -1490,15 +1491,15 @@
   using assms by (rule Max.hom_commute)
 
 lemma ab_semigroup_idem_mult_min:
-  "ab_semigroup_idem_mult min"
+  "class.ab_semigroup_idem_mult min"
   proof qed (auto simp add: min_def)
 
 lemma ab_semigroup_idem_mult_max:
-  "ab_semigroup_idem_mult max"
+  "class.ab_semigroup_idem_mult max"
   proof qed (auto simp add: max_def)
 
 lemma max_lattice:
-  "semilattice_inf (op \<ge>) (op >) max"
+  "class.semilattice_inf (op \<ge>) (op >) max"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max: