adapt to changes in generated transfer rules (cf. 4483c004499a)

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 16:53:24 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 17:54:47 2012 +0200
@@ -156,7 +156,7 @@
   apply (elim relcomppE)
   apply (rule relcomppI)
   apply (erule (1) map_transfer [THEN fun_relD, THEN fun_relD])
-  apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, OF refl])
+  apply (erule fmap.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl])
   done
 
 lemma ffilter_transfer [transfer_rule]:
@@ -166,7 +166,7 @@
   apply (elim relcomppE)
   apply (rule relcomppI)
   apply (erule (1) filter_transfer [THEN fun_relD, THEN fun_relD])
-  apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, OF refl])
+  apply (erule ffilter.transfer [THEN fun_relD, THEN fun_relD, unfolded relator_eq, OF refl])
   done
 
 lemma fset_transfer [transfer_rule]:
@@ -174,7 +174,7 @@
   unfolding cr_fset'_def
   apply (intro fun_relI)
   apply (elim relcomppE)
-  apply (drule fset.transfer [THEN fun_relD])
+  apply (drule fset.transfer [THEN fun_relD, unfolded relator_eq])
   apply (erule subst)
   apply (erule set_transfer [THEN fun_relD])
   done