diff -r 2008f1cf3030 -r f0a927235162 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Sat Mar 15 03:37:22 2014 +0100
+++ b/src/HOL/Predicate.thy	Sat Mar 15 08:31:33 2014 +0100
@@ -85,11 +85,11 @@
 
 lemma eval_INFI [simp]:
   "eval (INFI A f) = INFI A (eval \<circ> f)"
-  by (simp only: INF_def eval_Inf image_compose)
+  by (simp only: INF_def eval_Inf image_comp)
 
 lemma eval_SUPR [simp]:
   "eval (SUPR A f) = SUPR A (eval \<circ> f)"
-  by (simp only: SUP_def eval_Sup image_compose)
+  by (simp only: SUP_def eval_Sup image_comp)
 
 instantiation pred :: (type) complete_boolean_algebra
 begin