--- a/FSet.thy	Fri Dec 04 15:25:51 2009 +0100
+++ b/FSet.thy	Fri Dec 04 15:41:09 2009 +0100
@@ -276,7 +276,7 @@
 
 lemma ho_fold_rsp[quotient_rsp]:
   "(op = ===> op = ===> op = ===> op \<approx> ===> op =) fold1 fold1"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   apply (case_tac "rsp_fold x")
   prefer 2
   apply (erule_tac list_eq.induct)
@@ -456,14 +456,14 @@
 (* Probably not true without additional assumptions about the function *)
 lemma list_rec_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_rec list_rec"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   apply (erule_tac list_eq.induct)
   apply (simp_all)
   sorry
 
 lemma list_case_rsp[quotient_rsp]:
   "(op = ===> (op = ===> op \<approx> ===> op =) ===> op \<approx> ===> op =) list_case list_case"
-  apply (auto simp add: FUN_REL_EQ)
+  apply (auto)
   sorry
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}