--- a/src/HOL/Finite_Set.thy Mon Jun 25 15:14:07 2012 +0200
+++ b/src/HOL/Finite_Set.thy Mon Jun 25 17:41:20 2012 +0200
@@ -865,7 +865,7 @@
case (insert x F) then show ?case apply -
apply (simp add: subset_insert_iff, clarify)
apply (subgoal_tac "finite C")
- prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+ prefer 2 apply (blast dest: finite_subset [rotated])
apply (subgoal_tac "C = insert x (C - {x})")
prefer 2 apply blast
apply (erule ssubst)
@@ -1517,7 +1517,7 @@
apply - apply (erule finite_induct) apply simp
apply (simp add: subset_insert_iff, clarify)
apply (subgoal_tac "finite C")
- prefer 2 apply (blast dest: finite_subset [COMP swap_prems_rl])
+ prefer 2 apply (blast dest: finite_subset [rotated])
apply (subgoal_tac "C = insert x (C - {x})")
prefer 2 apply blast
apply (erule ssubst)