--- a/src/HOL/Library/Finite_Map.thy Mon Jan 22 11:23:42 2018 +0100
+++ b/src/HOL/Library/Finite_Map.thy Mon Jan 22 15:06:38 2018 +0100
@@ -331,9 +331,9 @@
qed
lemma fmfilter_cong'[fundef_cong]:
- assumes "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
- shows "fmfilter P m = fmfilter Q m"
-using assms
+ assumes "m = n" "\<And>x. x \<in> fmdom' m \<Longrightarrow> P x = Q x"
+ shows "fmfilter P m = fmfilter Q n"
+using assms(2) unfolding assms(1)
by (rule fmfilter_cong) (metis fmdom'I)
lemma fmfilter_upd[simp]:
@@ -1226,4 +1226,4 @@
lifting_update fmap.lifting
lifting_forget fmap.lifting
-end
+end
\ No newline at end of file