diff -r 08f3491c50bf -r 355a4cac5440 src/HOL/Library/Countable_Set.thy
--- a/src/HOL/Library/Countable_Set.thy	Tue Sep 03 19:58:00 2013 +0200
+++ b/src/HOL/Library/Countable_Set.thy	Tue Sep 03 22:04:23 2013 +0200
@@ -55,7 +55,8 @@
   assumes "countable S" "infinite S"
   obtains e :: "'a \<Rightarrow> nat" where "bij_betw e S UNIV"
 proof -
-  from `countable S`[THEN countableE] guess f .
+  obtain f :: "'a \<Rightarrow> nat" where "inj_on f S"
+    using `countable S` by (rule countableE)
   then have "bij_betw f S (f`S)"
     unfolding bij_betw_def by simp
   moreover
@@ -169,9 +170,12 @@
   "countable I \<Longrightarrow> (\<And>i. i \<in> I \<Longrightarrow> countable (A i)) \<Longrightarrow> countable (SIGMA i : I. A i)"
   by (intro countableI'[of "\<lambda>(i, a). (to_nat_on I i, to_nat_on (A i) a)"]) (auto simp: inj_on_def)
 
-lemma countable_image[intro, simp]: assumes A: "countable A" shows "countable (f`A)"
+lemma countable_image[intro, simp]:
+  assumes "countable A"
+  shows "countable (f`A)"
 proof -
-  from A guess g by (rule countableE)
+  obtain g :: "'a \<Rightarrow> nat" where "inj_on g A"
+    using assms by (rule countableE)
   moreover have "inj_on (inv_into A f) (f`A)" "inv_into A f ` f ` A \<subseteq> A"
     by (auto intro: inj_on_inv_into inv_into_into)
   ultimately show ?thesis