diff -r 5c2df04e97d1 -r 7ab8f003fe41 src/HOL/Library/Mapping.thy
--- a/src/HOL/Library/Mapping.thy	Thu Mar 06 15:25:21 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 15:29:18 2014 +0100
@@ -43,7 +43,7 @@
 
 lemma map_of_transfer [transfer_rule]:
   assumes [transfer_rule]: "bi_unique R1"
-  shows "(list_all2 (prod_rel R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
+  shows "(list_all2 (rel_prod R1 R2) ===> R1 ===> rel_option R2) map_of map_of"
 unfolding map_of_def by transfer_prover
 
 lemma tabulate_transfer: