--- a/src/HOL/Library/Mapping.thy Wed Aug 14 00:15:03 2013 +0200
+++ b/src/HOL/Library/Mapping.thy Tue Aug 13 18:22:55 2013 +0200
@@ -33,7 +33,7 @@
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
lemma [transfer_rule]: "(option_rel A ===> op=) equal_None equal_None"
-unfolding fun_rel_def option_rel_unfold equal_None_def by (auto split: option.split)
+unfolding fun_rel_def option_rel_def equal_None_def by (auto split: option.split)
lemma dom_transfer:
assumes [transfer_rule]: "bi_total A"