src/HOL/Library/Mapping.thy

--- a/src/HOL/Library/Mapping.thy	Thu Mar 06 14:25:55 2014 +0100
+++ b/src/HOL/Library/Mapping.thy	Thu Mar 06 14:57:14 2014 +0100
@@ -37,7 +37,7 @@
 
 lemma dom_transfer:
   assumes [transfer_rule]: "bi_total A"
-  shows "((A ===> rel_option B) ===> set_rel A) dom dom" 
+  shows "((A ===> rel_option B) ===> rel_set A) dom dom" 
 unfolding dom_def[abs_def] equal_None_def[symmetric] 
 by transfer_prover