diff -r f74a4175a3a8 -r 5e51075cbd97 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Thu Sep 08 08:41:28 2011 -0700
+++ b/src/HOL/Big_Operators.thy	Fri Sep 09 00:22:18 2011 +0200
@@ -1517,7 +1517,7 @@
   proof qed (auto simp add: max_def)
 
 lemma max_lattice:
-  "class.semilattice_inf (op \<ge>) (op >) max"
+  "class.semilattice_inf max (op \<ge>) (op >)"
   by (fact min_max.dual_semilattice)
 
 lemma dual_max:
@@ -1611,7 +1611,7 @@
   assumes "finite A" and "x \<in> A"
   shows "x \<le> Max A"
 proof -
-  interpret semilattice_inf "op \<ge>" "op >" max
+  interpret semilattice_inf max "op \<ge>" "op >"
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def fold1_belowI)
 qed
@@ -1625,7 +1625,7 @@
   assumes "finite A" and "A \<noteq> {}"
   shows "Max A \<le> x \<longleftrightarrow> (\<forall>a\<in>A. a \<le> x)"
 proof -
-  interpret semilattice_inf "op \<ge>" "op >" max
+  interpret semilattice_inf max "op \<ge>" "op >"
     by (rule max_lattice)
   from assms show ?thesis by (simp add: Max_def below_fold1_iff)
 qed