diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Transitive_Closure.thy
--- a/src/HOL/Transitive_Closure.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -82,7 +82,7 @@
 subsection {* Reflexive-transitive closure *}
 
 lemma reflcl_set_eq [pred_set_conv]: "(sup (\<lambda>x y. (x, y) \<in> r) op =) = (\<lambda>x y. (x, y) \<in> r \<union> Id)"
-  by (auto simp add: ext_iff)
+  by (auto simp add: fun_eq_iff)
 
 lemma r_into_rtrancl [intro]: "!!p. p \<in> r ==> p \<in> r^*"
   -- {* @{text rtrancl} of @{text r} contains @{text r} *}
@@ -186,7 +186,7 @@
 lemmas rtrancl_idemp [simp] = rtranclp_idemp [to_set]
 
 lemma rtrancl_idemp_self_comp [simp]: "R^* O R^* = R^*"
-  apply (rule set_ext)
+  apply (rule set_eqI)
   apply (simp only: split_tupled_all)
   apply (blast intro: rtrancl_trans)
   done
@@ -487,7 +487,7 @@
 lemmas trancl_converseD = tranclp_converseD [to_set]
 
 lemma tranclp_converse: "(r^--1)^++ = (r^++)^--1"
-  by (fastsimp simp add: ext_iff
+  by (fastsimp simp add: fun_eq_iff
     intro!: tranclp_converseI dest!: tranclp_converseD)
 
 lemmas trancl_converse = tranclp_converse [to_set]