--- a/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Apr 22 19:04:30 2012 +0200
+++ b/src/HOL/Quotient_Examples/Lift_FSet.thy Sun Apr 22 19:44:40 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 19:04:30 2012 +0200
+++ b/src/HOL/Tools/Lifting/lifting_def.ML Sun Apr 22 19:44:40 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