src/HOL/Analysis/Path_Connected.thy

       apply (auto dest: inj_onD [OF injg2])
       done
    } note ** = this
   show ?thesis
     using assms
-    apply (simp add: arc_def simple_path_def path_join, clarify)
+    apply (simp add: arc_def simple_path_def, clarify)
     apply (simp add: joinpaths_def split: if_split_asm)
     apply (force dest: inj_onD [OF injg1])
     apply (metis *)
     apply (metis **)
     apply (force dest: inj_onD [OF injg2])