--- a/src/HOL/Library/Countable_Set.thy Wed Aug 10 09:33:54 2016 +0200
+++ b/src/HOL/Library/Countable_Set.thy Wed Aug 10 14:50:59 2016 +0200
@@ -304,10 +304,9 @@
(is "?lhs = ?rhs")
proof
assume ?lhs
- then show ?rhs
- apply (rule_tac x="inv_into A f ` B" in exI)
- apply (auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into)
- done
+ show ?rhs
+ by (rule exI [where x="inv_into A f ` B"])
+ (use \<open>?lhs\<close> in \<open>auto simp: f_inv_into_f subset_iff image_inv_into_cancel inv_into_into\<close>)
next
assume ?rhs
then show ?lhs by force