--- a/src/HOL/Library/Mapping.thy Thu Mar 06 15:29:18 2014 +0100
+++ b/src/HOL/Library/Mapping.thy Thu Mar 06 15:40:33 2014 +0100
@@ -33,7 +33,7 @@
definition equal_None :: "'a option \<Rightarrow> bool" where "equal_None x \<equiv> x = None"
lemma [transfer_rule]: "(rel_option A ===> op=) equal_None equal_None"
-unfolding fun_rel_def rel_option_iff equal_None_def by (auto split: option.split)
+unfolding rel_fun_def rel_option_iff equal_None_def by (auto split: option.split)
lemma dom_transfer:
assumes [transfer_rule]: "bi_total A"
@@ -55,7 +55,7 @@
lemma bulkload_transfer:
"(list_all2 A ===> op= ===> rel_option A)
(\<lambda>xs k. if k < length xs then Some (xs ! k) else None) (\<lambda>xs k. if k < length xs then Some (xs ! k) else None)"
-unfolding fun_rel_def
+unfolding rel_fun_def
apply clarsimp
apply (erule list_all2_induct)
apply simp