--- a/src/HOL/Map.thy Wed Aug 18 23:04:58 2021 +0200
+++ b/src/HOL/Map.thy Thu Aug 19 12:31:06 2021 +0200
@@ -765,7 +765,7 @@
unfolding graph_eq_to_snd_dom finite_dom_map_of
using finite_dom_map_of by blast
-lemma graph_map_of_if_distinct_ran: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
+lemma graph_map_of_if_distinct_dom: "distinct (map fst al) \<Longrightarrow> graph (map_of al) = set al"
unfolding graph_def by auto
lemma finite_graph_iff_finite_dom[simp]: "finite (graph m) = finite (dom m)"