--- a/src/HOL/Library/Product_Order.thy Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Library/Product_Order.thy Sat Mar 15 08:31:33 2014 +0100
@@ -225,10 +225,10 @@
by (auto simp: Sup_prod_def SUP_def)
lemma INFI_prod_alt_def: "INFI A f = (INFI A (fst o f), INFI A (snd o f))"
-by (auto simp: INF_def Inf_prod_def image_compose)
+by (auto simp: INF_def Inf_prod_def image_comp)
lemma SUPR_prod_alt_def: "SUPR A f = (SUPR A (fst o f), SUPR A (snd o f))"
-by (auto simp: SUP_def Sup_prod_def image_compose)
+by (auto simp: SUP_def Sup_prod_def image_comp)
lemma INF_prod_alt_def:
"(INF x:A. f x) = (INF x:A. fst (f x), INF x:A. snd (f x))"