diff -r a0fd8c2db293 -r 86a3557a9ebb src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Aug 20 18:07:28 2007 +0200
+++ b/src/HOL/Predicate.thy	Mon Aug 20 18:07:29 2007 +0200
@@ -134,10 +134,10 @@
 subsection {* Unions of families *}
 
 lemma SUP1_iff [simp]: "(SUP x:A. B x) b = (EX x:A. B x b)"
-  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
+  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
 lemma SUP2_iff [simp]: "(SUP x:A. B x) b c = (EX x:A. B x b c)"
-  by (simp add: SUPR_def Sup_fun_eq Sup_bool_eq) blast
+  by (simp add: SUPR_def Sup_fun_def Sup_bool_def) blast
 
 lemma SUP1_I [intro]: "a : A ==> B a b ==> (SUP x:A. B x) b"
   by auto