# HG changeset patch
# User huffman
# Date 1335110087 -7200
# Node ID ec235f56444416b8a5bf654b55561686de1cab6d
# Parent  4483c004499ac7e93922e89f90cad2b8df8e491e
adapt to changes in generated transfer rules (cf. 4483c004499a)

diff -r 4483c004499a -r ec235f564444 src/HOL/Quotient_Examples/Lift_FSet.thy
--- 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