src/HOL/Library/Lub_Glb.thy

--- a/src/HOL/Library/Lub_Glb.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Lub_Glb.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -230,7 +230,7 @@
     by (intro LIMSEQ_incseq_SUP) (auto simp: incseq_def image_def eq_commute bdd_above_setle)
   also have "(SUP i. X i) = u"
     using isLub_cSup[of "range X"] u[THEN isLubD1]
-    by (intro isLub_unique[OF _ u]) (auto simp add: SUP_def image_def eq_commute)
+    by (intro isLub_unique[OF _ u]) (auto simp add: image_def eq_commute)
   finally show ?thesis .
 qed