--- a/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Jun 25 15:14:07 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Path_Connected.thy Mon Jun 25 17:41:20 2012 +0200
@@ -511,7 +511,7 @@
hence "path_component (S i) x z" and "path_component (S j) z y"
using assms by (simp_all add: path_connected_component)
hence "path_component (\<Union>i\<in>A. S i) x z" and "path_component (\<Union>i\<in>A. S i) z y"
- using *(1,3) by (auto elim!: path_component_of_subset [COMP swap_prems_rl])
+ using *(1,3) by (auto elim!: path_component_of_subset [rotated])
thus "path_component (\<Union>i\<in>A. S i) x y"
by (rule path_component_trans)
qed