diff -r 1898e61e89c4 -r adac34829e10 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Jan 10 18:12:03 2012 +0100
+++ b/src/HOL/Wellfounded.thy	Tue Jan 10 18:12:55 2012 +0100
@@ -298,7 +298,7 @@
 
 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)"
-  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred SUP_UN_eq2])
+  apply (rule wf_UN [where I=UNIV and r="\<lambda>i. {(x, y). r i x y}", to_pred])
   apply (simp_all add: inf_set_def)
   apply auto
   done
@@ -611,9 +611,9 @@
 
 lemmas wf_acc_iff = wfP_accp_iff [to_set]
 
-lemmas acc_subset = accp_subset [to_set pred_subset_eq]
+lemmas acc_subset = accp_subset [to_set]
 
-lemmas acc_subset_induct = accp_subset_induct [to_set pred_subset_eq]
+lemmas acc_subset_induct = accp_subset_induct [to_set]
 
 
 subsection {* Tools for building wellfounded relations *}