# HG changeset patch
# User haftmann
# Date 1253716373 -7200
# Node ID 6f0a56d255f43ec656148881189a0713369ad243
# Parent  7f9e05b3d0fb33ff75f7ebd6b3fae2d1fc8e8579
simplified proof

diff -r 7f9e05b3d0fb -r 6f0a56d255f4 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Wed Sep 23 16:32:53 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Sep 23 16:32:53 2009 +0200
@@ -267,8 +267,8 @@
 
 lemma wfP_SUP:
   "\<forall>i. wfP (r i) \<Longrightarrow> \<forall>i j. r i \<noteq> r j \<longrightarrow> inf (DomainP (r i)) (RangeP (r j)) = bot \<Longrightarrow> wfP (SUPR UNIV r)"
-  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2 pred_equals_eq])
-    (simp_all add: bot_fun_eq bot_bool_eq)
+  by (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
+    (simp_all add: Collect_def)
 
 lemma wf_Union: 
  "[| ALL r:R. wf r;