diff -r 19efc2af3e6c -r f967a16dfcdd src/HOL/Library/Quotient_Option.thy
--- a/src/HOL/Library/Quotient_Option.thy	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Library/Quotient_Option.thy	Tue Sep 07 10:05:19 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: expand_fun_eq)
+  apply(simp add: ext_iff)
   apply(simp add: Quotient_abs_rep[OF q])
   done
 
 lemma option_map_id[id_simps]:
   shows "Option.map id = id"
-  by (simp add: expand_fun_eq split_option_all)
+  by (simp add: ext_iff split_option_all)
 
 lemma option_rel_eq[id_simps]:
   shows "option_rel (op =) = (op =)"
-  by (simp add: expand_fun_eq split_option_all)
+  by (simp add: ext_iff split_option_all)
 
 end