diff -r 82f57315cade -r 7a92cbec7030 src/HOL/Fun.thy
--- 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)"