--- a/src/HOL/Fun.thy Sun Jan 20 17:15:49 2019 +0000
+++ b/src/HOL/Fun.thy Mon Jan 21 14:44:23 2019 +0000
@@ -181,7 +181,7 @@
lemma inj_on_strict_subset: "inj_on f B \<Longrightarrow> A \<subset> B \<Longrightarrow> f ` A \<subset> f ` B"
unfolding inj_on_def by blast
-lemma inj_comp: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
+lemma inj_compose: "inj f \<Longrightarrow> inj g \<Longrightarrow> inj (f \<circ> g)"
by (simp add: inj_def)
lemma inj_fun: "inj f \<Longrightarrow> inj (\<lambda>x y. f x)"