diff -r 3d44892ac0d6 -r f30e941b4512 src/HOL/Big_Operators.thy
--- a/src/HOL/Big_Operators.thy	Tue Mar 13 16:22:18 2012 +0100
+++ b/src/HOL/Big_Operators.thy	Tue Mar 13 16:40:06 2012 +0100
@@ -1537,11 +1537,11 @@
 
 lemma dual_max:
   "ord.max (op \<ge>) = min"
-  by (auto simp add: ord.max_def_raw min_def fun_eq_iff)
+  by (auto simp add: ord.max_def min_def fun_eq_iff)
 
 lemma dual_min:
   "ord.min (op \<ge>) = max"
-  by (auto simp add: ord.min_def_raw max_def fun_eq_iff)
+  by (auto simp add: ord.min_def max_def fun_eq_iff)
 
 lemma strict_below_fold1_iff:
   assumes "finite A" and "A \<noteq> {}"