diff -r 54f16a0a3069 -r a949b2a5f51d src/HOL/Multivariate_Analysis/Path_Connected.thy
--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:22:02 2016 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy	Fri May 13 20:24:10 2016 +0200
@@ -1318,7 +1318,6 @@
   by (auto intro!: path_component_mem path_component_refl)
 
 lemma path_component_sym: "path_component s x y \<Longrightarrow> path_component s y x"
-  using assms
   unfolding path_component_def
   apply (erule exE)
   apply (rule_tac x="reversepath g" in exI)