--- a/src/HOL/Library/Finite_Map.thy Tue May 22 14:12:15 2018 +0200
+++ b/src/HOL/Library/Finite_Map.thy Tue May 22 11:08:37 2018 +0200
@@ -84,10 +84,10 @@
definition map_filter :: "('a \<Rightarrow> bool) \<Rightarrow> ('a \<rightharpoonup> 'b) \<Rightarrow> ('a \<rightharpoonup> 'b)" where
"map_filter P m = (\<lambda>x. if P x then m x else None)"
-lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of [(k, _) \<leftarrow> m. P k]"
+lemma map_filter_map_of[simp]: "map_filter P (map_of m) = map_of (filter (\<lambda>(k, _). P k) m)"
proof
fix x
- show "map_filter P (map_of m) x = map_of [(k, _) \<leftarrow> m. P k] x"
+ show "map_filter P (map_of m) x = map_of (filter (\<lambda>(k, _). P k) m) x"
by (induct m) (auto simp: map_filter_def)
qed