FSet: Explicit proof without mem_def

--- a/src/HOL/Quotient_Examples/FSet.thy	Thu Aug 25 19:09:39 2011 +0200
+++ b/src/HOL/Quotient_Examples/FSet.thy	Fri Aug 26 09:31:56 2011 +0900
@@ -196,7 +196,11 @@
 
 lemma member_rsp [quot_respect]:
   shows "(op \<approx> ===> op =) List.member List.member"
-  by (auto intro!: fun_relI simp add: mem_def)
+proof
+  fix x y assume "x \<approx> y"
+  then show "List.member x = List.member y"
+    unfolding fun_eq_iff by simp
+qed
 
 lemma nil_rsp [quot_respect]:
   shows "(op \<approx>) Nil Nil"