diff -r 10cd49e0c067 -r 66f1a0dfe7d9 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Fri Aug 28 18:52:41 2009 +0200
+++ b/src/HOL/OrderedGroup.thy	Fri Aug 28 19:15:59 2009 +0200
@@ -1275,7 +1275,7 @@
 proof -
   note add_le_cancel_right [of a a "- a", symmetric, simplified]
   moreover note add_le_cancel_right [of "-a" a a, symmetric, simplified]
-  then show ?thesis by (auto simp: sup_max max_def)
+  then show ?thesis by (auto simp: sup_max)
 qed
 
 lemma abs_if_lattice: