merged

--- a/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 16:33:41 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy	Sun Apr 22 19:18:26 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

--- a/src/HOL/Tools/Lifting/lifting_def.ML	Sun Apr 22 16:33:41 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML	Sun Apr 22 19:18:26 2012 +0200
@@ -191,7 +191,7 @@
     val ((_, (_ , def_thm)), lthy') = 
       Local_Theory.define (var, ((Thm.def_binding (#1 var), []), newrhs)) lthy
 
-    val transfer_thm = [quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer}
+    val transfer_thm = ([quotient_thm, rsp_thm, def_thm] MRSL @{thm Quotient_to_transfer})
         |> Raw_Simplifier.rewrite_rule (Transfer.get_relator_eq lthy')
 
     fun qualify defname suffix = Binding.qualified true suffix defname