1.1 --- a/src/HOL/Finite_Set.thy	Mon Jun 25 15:14:07 2012 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Mon Jun 25 17:41:20 2012 +0200
     1.3 @@ -865,7 +865,7 @@
     1.4      case (insert x F) then show ?case apply -
     1.5      apply (simp add: subset_insert_iff, clarify)
     1.6      apply (subgoal_tac "finite C")
     1.7 -      prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
     1.8 +      prefer 2 apply (blast dest: finite_subset [rotated])
     1.9      apply (subgoal_tac "C = insert x (C - {x})")
    1.10        prefer 2 apply blast
    1.11      apply (erule ssubst)
    1.12 @@ -1517,7 +1517,7 @@
    1.13    apply - apply (erule finite_induct) apply simp
    1.14    apply (simp add: subset_insert_iff, clarify)
    1.15    apply (subgoal_tac "finite C")
    1.16 -  prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
    1.17 +  prefer 2 apply (blast dest: finite_subset [rotated])
    1.18    apply (subgoal_tac "C = insert x (C - {x})")
    1.19    prefer 2 apply blast
    1.20    apply (erule ssubst)

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

     3.1 --- a/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 15:14:07 2012 +0200
     3.2 +++ b/src/HOL/Multivariate_Analysis/Topology_Euclidean_Space.thy	Mon Jun 25 17:41:20 2012 +0200
     3.3 @@ -4208,7 +4208,7 @@
     3.4  apply (rule_tac x="(l1, l2)" in rev_bexI, simp)
     3.5  apply (rule_tac x="r1 \<circ> r2" in exI)
     3.6  apply (rule conjI, simp add: subseq_def)
     3.7 -apply (drule_tac r=r2 in lim_subseq [COMP swap_prems_rl], assumption)
     3.8 +apply (drule_tac r=r2 in lim_subseq [rotated], assumption)
     3.9  apply (drule (1) tendsto_Pair) back
    3.10  apply (simp add: o_def)
    3.11  done