diff -r f9f3006a5579 -r e690d6f2185b src/HOL/Library/Countable_Set.thy
--- 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