diff -r 63eb6b3ebcfc -r ad84f8a712b4 src/HOL/Analysis/Brouwer_Fixpoint.thy
--- a/src/HOL/Analysis/Brouwer_Fixpoint.thy	Fri Apr 10 22:51:18 2020 +0100
+++ b/src/HOL/Analysis/Brouwer_Fixpoint.thy	Sun Apr 12 10:51:51 2020 +0100
@@ -149,7 +149,7 @@
     apply (rule_tac x=r in exI, simp)
      apply (rule homotopic_with_trans, assumption)
      apply (rule_tac f = "r \<circ> f" and g="r \<circ> id" in homotopic_with_eq)
-        apply (rule_tac Y=S in homotopic_compose_continuous_left)
+        apply (rule_tac Y=S in homotopic_with_compose_continuous_left)
          apply (auto simp: homotopic_with_sym)
     done
 qed