diff -r eec472dae593 -r 154dc6ec0041 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Mon Mar 12 15:12:22 2012 +0100
+++ b/src/HOL/Predicate.thy	Mon Mar 12 21:41:11 2012 +0100
@@ -123,7 +123,7 @@
   by (simp add: minus_pred_def)
 
 instance proof
-qed (auto intro!: pred_eqI simp add: uminus_apply minus_apply INF_apply SUP_apply)
+qed (auto intro!: pred_eqI)
 
 end
 
@@ -143,7 +143,7 @@
 
 lemma bind_bind:
   "(P \<guillemotright>= Q) \<guillemotright>= R = P \<guillemotright>= (\<lambda>x. Q x \<guillemotright>= R)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma bind_single:
   "P \<guillemotright>= single = P"
@@ -163,7 +163,7 @@
 
 lemma Sup_bind:
   "(\<Squnion>A \<guillemotright>= f) = \<Squnion>((\<lambda>x. x \<guillemotright>= f) ` A)"
-  by (rule pred_eqI) (auto simp add: SUP_apply)
+  by (rule pred_eqI) auto
 
 lemma pred_iffI:
   assumes "\<And>x. eval A x \<Longrightarrow> eval B x"