diff -r e1bd8a54c40f -r d7728f65b353 src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Mon Sep 13 08:43:48 2010 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Mon Sep 13 11:13:15 2010 +0200
@@ -66,16 +66,16 @@
 lemma option_Some_prs[quot_preserve]:
   assumes q: "Quotient R Abs Rep"
   shows "(Rep ---> Option.map Abs) Some = Some"
-  apply(simp add: ext_iff)
+  apply(simp add: fun_eq_iff)
   apply(simp add: Quotient_abs_rep[OF q])
   done
 
 lemma option_map_id[id_simps]:
   shows "Option.map id = id"
-  by (simp add: ext_iff split_option_all)
+  by (simp add: fun_eq_iff split_option_all)
 
 lemma option_rel_eq[id_simps]:
   shows "option_rel (op =) = (op =)"
-  by (simp add: ext_iff split_option_all)
+  by (simp add: fun_eq_iff split_option_all)
 
 end